Stefan Pranger 
							
						 
						
							
							
							
								
							
								3f2aaf72b0 
								
							
								 
							
						 
						
							
							
								
								fixed typo in arg list of GameFormula  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								2721f24b9b 
								
							
								 
							
						 
						
							
							
								
								added Coalition default ctor  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								487eb13a24 
								
							
								 
							
						 
						
							
							
								
								WIP added grammar rules for gameFormula  
							
							
 
							
							
							Does not compile at this stage! This commit will be squashed asap. 
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								df52e5af88 
								
							
								 
							
						 
						
							
							
								
								added casting getter for gameFormula  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								2f5a53196c 
								
							
								 
							
						 
						
							
							
								
								added rPATL to FragmentSpecifitcations  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								7d87a90c1e 
								
							
								 
							
						 
						
							
							
								
								added multiple Visitor methods for gameFormulas  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								09cb1d465c 
								
							
								 
							
						 
						
							
							
								
								added GameFormula class  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								310c9d21d4 
								
							
								 
							
						 
						
							
							
								
								added Coalition class  
							
							
 
							
							
							will be used in rPATL formulas 
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								bc5eec34d2 
								
							
								 
							
						 
						
							
							
								
								switch cases in engine now feature SMG case  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								875410a59e 
								
							
								 
							
						 
						
							
							
								
								Polished ExplicitModelBuilder:  
							
							
 
							
							
							* ChoiceInformationBuilder renamed to StateAndChoiceInformationBuilder, now also keeping track of state-based information (StateValuations, MarkovianStates, statePlayerIndications)
* ModelComponents now consider statePlayerIndications and PlayerNamesToIndices separately 
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								277f802850 
								
							
								 
							
						 
						
							
							
								
								* PlayerIndex is now declared in a separate file (as this can potentially be independent of PRISM input).  
							
							
 
							
							
							* Polished PrismNextStateGenerator, in particular more proper error handling 
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
								
								
							
							
								
							
								3ba9ae637c 
								
									
								
							
								 
							
						 
						
							
							
								
								Run doxygen deploy on push and do not keep history  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d2c6420356 
								
							
								 
							
						 
						
							
							
								
								Add doxygen deploy workflow  
							
							
 
							
							
							currently manually triggered 
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								df721f55d7 
								
							
								 
							
						 
						
							
							
								
								Cleanup comments  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								97b2d751e0 
								
							
								 
							
						 
						
							
							
								
								* prism::Player's no longer keep track of module and action indices to reduce redundancies.  
							
							
 
							
							
							* PrismProgram::CheckValidity and PrismProgram::simplify now treat SMGs properly
* PrismProgram is now responsible for moduleIndex->playerIndex and actionIndex->playerIndex assignment
* More defined behavior for actions that don't have a player (work in progress) 
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6fe76a009d 
								
							
								 
							
						 
						
							
							
								
								Polished parsing of Prism-SMGs, in particular  
							
							
 
							
							
							* Fixed issues related to module renaming that resulted from setting the module indices already in the first run
  * Fixed a few uint_fast32_t vs uint_fast64_t issues, created alias PlayerIndex 
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								81db530f70 
								
							
								 
							
						 
						
							
							
								
								do not clear moduleToIndexMap for second run  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								52e30059e3 
								
							
								 
							
						 
						
							
							
								
								fix reorder warning  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e529045a8f 
								
							
								 
							
						 
						
							
							
								
								Merge commit '6a71c19d8a5808b3a0c5be21f0966e8ada7f4252' into smg-merge  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
								
								
							
							
								
							
								e610edc197 
								
									
								
							
								 
							
						 
						
							
							
								
								Run github actions daily  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								741d04c797 
								
							
								 
							
						 
						
							
							
								
								Implement manually triggered github actions CI  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								02695da9b7 
								
							
								 
							
						 
						
							
							
								
								Fixed several issues regarding powers with negative exponents.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a3ada8a0c3 
								
							
								 
							
						 
						
							
							
								
								cli: added a space that was missing in output of steady-state result  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4dcd1cfb64 
								
							
								 
							
						 
						
							
							
								
								Fixed simplification of expressions that use the power operator with negative exponents.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								09cb0e5a5d 
								
							
								 
							
						 
						
							
							
								
								LraCtmcTest: Renamed a testcase as its name was misleading before.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5245d77bfc 
								
							
								 
							
						 
						
							
							
								
								SteadyState: Issue a warning in sound mode because it is not supported.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								818f8cb8ee 
								
							
								 
							
						 
						
							
							
								
								steadystate: Added a testcase.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b73e2e5d1c 
								
							
								 
							
						 
						
							
							
								
								Fixing steady state distribution computation.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								77d2e9c98f 
								
							
								 
							
						 
						
							
							
								
								Fixed output of steady-state distr computation.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								211a72b6d7 
								
							
								 
							
						 
						
							
							
								
								fixing compilation of storm-pars  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								19e6473806 
								
							
								 
							
						 
						
							
							
								
								making the cudd warning sound a bit less dangerous  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2e593dc014 
								
							
								 
							
						 
						
							
							
								
								Added computation of steady state probabilities for DTMC/CTMC in the sparse engine.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								28ab011eb8 
								
							
								 
							
						 
						
							
							
								
								Added an export of check results to json.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								84e6984659 
								
							
								 
							
						 
						
							
							
								
								StateValuations::toJson now has a template parameter to change the exported type of rationals.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								75b6ac27e8 
								
							
								 
							
						 
						
							
							
								
								JaniParser: Making result field optional ( fixes   #83 )  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3184ba1611 
								
							
								 
							
						 
						
							
							
								
								Jani: Correctly parse the input-enable field. Throw an error in the sparse model builder, as these are not supported right now.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								41ae9d5624 
								
							
								 
							
						 
						
							
							
								
								Fixed silently truncating bits when parsing integer literal expressions (see  https://github.com/moves-rwth/stormpy/issues/20 )  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								51f86db9eb 
								
							
								 
							
						 
						
							
							
								
								Storm version 1.6.3  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7002946845 
								
							
								 
							
						 
						
							
							
								
								Updated changelog.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								251527bccf 
								
							
								 
							
						 
						
							
							
								
								storm-pars: Make a more explicit warning if a non-parametric equation solver type is selected.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1243feba8c 
								
							
								 
							
						 
						
							
							
								
								Substitute constants in JANI Properties ( fixes   #95 )  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								065b366198 
								
							
								 
							
						 
						
							
							
								
								Removed superfluous '.' in output of Markov automata model data.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6d6e142236 
								
							
								 
							
						 
						
							
							
								
								Fixed an issue with JANI models concerning properties using transient variable expressions.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ee5fff680a 
								
							
								 
							
						 
						
							
							
								
								Indefinite Horizon helpers: Do not compute values of MaybeStates if they are not relevant for the property. ( Fixes   #87 )  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								20d424e289 
								
							
								 
							
						 
						
							
							
								
								JaniTraverser: Only traverse lower/upper bound expressions of BoundedIntegerVariables, if these bounds exists.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ce0283d80d 
								
							
								 
							
						 
						
							
							
								
								Cmake: checked whether the stack-check issue still persists with current AppleClang v12.0.0  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8619a4d833 
								
							
								 
							
						 
						
							
							
								
								CMake: Implemented a workaround for building CUDD on MacOS Big Sur.  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1982dc0dba 
								
							
								 
							
						 
						
							
							
								
								SparsePcaaParetoQuery: Added a (hopefully explaining) comment  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								6a71c19d8a 
								
							
								 
							
						 
						
							
							
								
								added sparse smg model  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								bb05b9c03c 
								
							
								 
							
						 
						
							
							
								
								aggregate player indices into model  
							
							
								
 
							
							
						 
						5 years ago