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  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								cea09f932b 
								
							
								 
							
						 
						
							
							
								
								generator now assigns player indices to states  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								163dfa8654 
								
							
								 
							
						 
						
							
							
								
								ModelComponents now feature a player mapping  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								6b715792aa 
								
							
								 
							
						 
						
							
							
								
								added player related helpers  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								160a2c32a2 
								
							
								 
							
						 
						
							
							
								
								added SMGs to existing ModelTypes  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								dce9496300 
								
							
								 
							
						 
						
							
							
								
								Model validity check now handles SMGs  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								9bf2a572a7 
								
							
								 
							
						 
						
							
							
								
								check if state is controlled by multiple players  
							
							
 
							
							
							We do this by storing a list of modules/commands which have already been claimed by one player 
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								e9a6077acb 
								
							
								 
							
						 
						
							
							
								
								adapted player ostream output  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								1cf2e544ac 
								
							
								 
							
						 
						
							
							
								
								add assertion for module indices in second  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								de301323d6 
								
							
								 
							
						 
						
							
							
								
								check module and action names when parsing players  
							
							
 
							
							
							Note: This does currently not work as intended as the moduleToIndexMap
gets clear when moving to the second run! 
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								43353d5243 
								
							
								 
							
						 
						
							
							
								
								store name index map for player member  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								271ed284a6 
								
							
								 
							
						 
						
							
							
								
								fix player ostream output  
							
							
								
 
							
							
						 
						5 years ago  
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								11f7464372 
								
							
								 
							
						 
						
							
							
								
								players now get stored in PRISM programs  
							
							
								
 
							
							
						 
						5 years ago