cb89ab7509 
								
							
								 
							
						 
						
							
							
								
								clearing end-component requirement in topological solver  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9aaf7e0bfb 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into chris_diss  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a616e2743d 
								
							
								 
							
						 
						
							
							
								
								fixes to standard-compliant prism-to-jani conversion  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e64e293d59 
								
							
								 
							
						 
						
							
							
								
								jani transformer which changes a variable into a location  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f9e4208268 
								
							
								 
							
						 
						
							
							
								
								export jani with comment expressions to ease debugging jani models  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6275c52779 
								
							
								 
							
						 
						
							
							
								
								several convenience additions to jani data structures  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								33c189bd32 
								
							
								 
							
						 
						
							
							
								
								export setting for flattening  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a46e6439eb 
								
							
								 
							
						 
						
							
							
								
								enabled switching of methods if unsupported method chosen in symbolic min-max equation solver  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9ed6f084e7 
								
							
								 
							
						 
						
							
							
								
								adding uniqueness constraint in LRA computation also for fixed-point formulation  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b73f0ef94e 
								
							
								 
							
						 
						
							
							
								
								fixing issue in jani-to-prism label replacement  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9d528db2fc 
								
							
								 
							
						 
						
							
							
								
								adding translation of expressions used in formulas to symbolic-to-sparse transformers  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0c0f61e27b 
								
							
								 
							
						 
						
							
							
								
								Fix: Only access counterexample settings in model-handling, if they are available.  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e609a240a9 
								
							
								 
							
						 
						
							
							
								
								selecting minmax topological by default  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4500f98ae1 
								
							
								 
							
						 
						
							
							
								
								fixing typo  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a7caf709ae 
								
							
								 
							
						 
						
							
							
								
								default to topological equation solver  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dff67450e0 
								
							
								 
							
						 
						
							
							
								
								fixed recently introduced bug in JANI export  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8114437cee 
								
							
								 
							
						 
						
							
							
								
								allowing cumulative and instantaneous reward properties to be transformed to JANI  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d638972bc8 
								
							
								 
							
						 
						
							
							
								
								enabled pushing location assignments to edges  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								749ba87254 
								
							
								 
							
						 
						
							
							
								
								Made SVI log output more clear  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								db6f43ed9d 
								
							
								 
							
						 
						
							
							
								
								made LRA computation for deterministic systems able to respect that the underlying solver requires a fixed-point formulation  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								86069b8552 
								
							
								 
							
						 
						
							
							
								
								fix typo in JSON exporter  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								50aa6d1424 
								
							
								 
							
						 
						
							
							
								
								assuming the only global real transient variable is the reward when exporting JANI and no reward model is mentioned in the property (issues a warning)  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c4bed85dc4 
								
							
								 
							
						 
						
							
							
								
								switching to native linear equation solver by default and power iteration  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1f6fc7e273 
								
							
								 
							
						 
						
							
							
								
								Better conversion of MA to CTMC if there are only Markovian states  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ca2295be1d 
								
							
								 
							
						 
						
							
							
								
								updated changelog: support for expected total rewards  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5a16b2befa 
								
							
								 
							
						 
						
							
							
								
								minor fixes to let the total reward tests compile and pass  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1f4c0325be 
								
							
								 
							
						 
						
							
							
								
								test cases for ctmcs and markov automata  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8df9b461cb 
								
							
								 
							
						 
						
							
							
								
								total reward formulas for ctmcs and markov automata  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b5566fa861 
								
							
								 
							
						 
						
							
							
								
								more on total reward formulas for mdps  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b3edae8707 
								
							
								 
							
						 
						
							
							
								
								fixed fragment specification: total reward formulas should not be supported for hybrid/dd right now  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c2dd57cda5 
								
							
								 
							
						 
						
							
							
								
								total rewards for mdps  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								87e34d7b32 
								
							
								 
							
						 
						
							
							
								
								Added Support for Total Reward Formulas for DTMCs in the Sparse Engine  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dfc0141894 
								
							
								 
							
						 
						
							
							
								
								minor fix to Z3 API modification  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cdfa328464 
								
							
								 
							
						 
						
							
							
								
								first attempt at adapting to Z3 interface change  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a6e6d5993f 
								
							
								 
							
						 
						
							
							
								
								Travis: set unlimited clone depth to allow versioning with git describe  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								afb0be1245 
								
							
								 
							
						 
						
							
							
								
								Fixed missing dependencies to storm-parsers  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9e398ffaab 
								
							
								 
							
						 
						
							
							
								
								Minor improvements for some CMake output  
							
							
								
 
							
							
						 
						7 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								53238f43f7 
								
							
								 
							
						 
						
							
							
								
								fixed some missing includes due to updated API  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								39698d6ecb 
								
							
								 
							
						 
						
							
							
								
								fix install of storm-counterexamples  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								79bb6734ed 
								
							
								 
							
						 
						
							
							
								
								compile and link parsers in seperate binary  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3a704ae532 
								
							
								 
							
						 
						
							
							
								
								fix storm-dft missing includes  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6dfce6a405 
								
							
								 
							
						 
						
							
							
								
								extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6fcc91b9d0 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://srv-i2.informatik.rwth-aachen.de/scm/git/storm  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d1ab260068 
								
							
								 
							
						 
						
							
							
								
								remove outdated parts in highlevel counterexamplse  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e29e6c7cd2 
								
							
								 
							
						 
						
							
							
								
								high level counterexamples extended with more options, and improved performance when minimizing over a subset  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ade4b5bf72 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://srv-i2.informatik.rwth-aachen.de/scm/git/storm  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b6d67e7995 
								
							
								 
							
						 
						
							
							
								
								properties.cpp: Output warning if we filter away all properties  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2948611f3f 
								
							
								 
							
						 
						
							
							
								
								cli.cpp: Quote arguments in "Command line arguments" status line  
							
							
 
							
							
							It's nice to be able to copy-paste the arguments from a log file to a shell,
so we'd like to have proper quoting.
We thus use single quotes if an argument contains non-safe characters
in the log output. 
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								04a1bbedfc 
								
							
								 
							
						 
						
							
							
								
								properties.cpp: Log filename of properties file in --verbose mode  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								30a95ef9d6 
								
							
								 
							
						 
						
							
							
								
								Simplify check whether argument of --prop is a file/property  
							
							
 
							
							
							Before, the argument to `--prop` was only treated as a file if (a) it exits and (b) contains a dot.
We remove the requirement for a dot and always treat the argument as a file if it exists. 
							
						 
						8 years ago