977dd1ef53 
								
							
								 
							
						 
						
							
							
								
								Get GMP location from carl, set it as a hint for sylvan.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a371301312 
								
							
								 
							
						 
						
							
							
								
								We require gmp, so we can as well just set the corresponding flag to true.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1c22fdabe1 
								
							
								 
							
						 
						
							
							
								
								Edit in Sylvan/cmake: Allow for hints about gmp location  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								97a7689c67 
								
							
								 
							
						 
						
							
							
								
								gcc and clang working on Debian Stretch again  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6d9e906291 
								
							
								 
							
						 
						
							
							
								
								remove LTO from sylvan as it causes more problems than it solves  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ec3468aef5 
								
							
								 
							
						 
						
							
							
								
								hopefully fixed the compile issue on Linux  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4e1855a440 
								
							
								 
							
						 
						
							
							
								
								use of intermediate value to make conversion work with gmp  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bae4b421ab 
								
							
								 
							
						 
						
							
							
								
								added missing template instantiation and print more info on LTO in cmake  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8bfa699519 
								
							
								 
							
						 
						
							
							
								
								attempt to fix link error  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cd954aacd9 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://srv-i2.informatik.rwth-aachen.de/scm/git/storm  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								233c063ad8 
								
							
								 
							
						 
						
							
							
								
								statistics output for multi-obj model checking when -stats option is given  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2e01c8b137 
								
							
								 
							
						 
						
							
							
								
								Fixed time bounds containing constant variables for multi objective formulas.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6598c2707c 
								
							
								 
							
						 
						
							
							
								
								Merge remote-tracking branch 'origin/master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9f795ffccd 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								187e8bc52b 
								
							
								 
							
						 
						
							
							
								
								fixed two bugs related to hybrid quantitative results  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a896c0df28 
								
							
								 
							
						 
						
							
							
								
								improved exact computations  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								09552d43a3 
								
							
								 
							
						 
						
							
							
								
								IsExact number trait  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ee754c96e2 
								
							
								 
							
						 
						
							
							
								
								renamed ParameterLifting.h -> RegionChecker.h  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ab7b31b08c 
								
							
								 
							
						 
						
							
							
								
								optimized memory requirements when a large amount of regions is to be analyzed. Also: Progress bar :)  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2647ffa9ae 
								
							
								 
							
						 
						
							
							
								
								added test for exact validations  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d659d193bc 
								
							
								 
							
						 
						
							
							
								
								Fixed game solver test and potential memory leaks  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2cdda140b8 
								
							
								 
							
						 
						
							
							
								
								Minor updates to ExprTk  
							
							
 
							
							
							Updated multi-sub expression operator to return final sub-expression type.
Updates to exprtk_disable_return_statement macro for disabling return statements and associated exceptions at the source code level. 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								de87ff1152 
								
							
								 
							
						 
						
							
							
								
								fixed finding of z3 library when its location is given via -DZ3_ROOT  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f59e9a7f77 
								
							
								 
							
						 
						
							
							
								
								added flushing of cout in STORM_PRINT macro  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								367b8f0a3e 
								
							
								 
							
						 
						
							
							
								
								parameter lifting with hybrid engine  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bb3c2bd556 
								
							
								 
							
						 
						
							
							
								
								Implemented policy iteration for game solver  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0d9205c0e6 
								
							
								 
							
						 
						
							
							
								
								Fixed case in include path  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								00c210565b 
								
							
								 
							
						 
						
							
							
								
								Merge from dft_case_study  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e05672a87d 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								936293e318 
								
							
								 
							
						 
						
							
							
								
								Refactored GameSolver. It is now analogous to the MinMaxLinearEquationSolver.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								77e71b7876 
								
							
								 
							
						 
						
							
							
								
								capitalization error and fix for cumulative rewards  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c16390e7f5 
								
							
								 
							
						 
						
							
							
								
								Equality Comparisons for JaniVars, just to make life easier :-)  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3eb675f8c0 
								
							
								 
							
						 
						
							
							
								
								used helper methods instead of own implementations  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								502cf4d6e0 
								
							
								 
							
						 
						
							
							
								
								extended model checker hint functionality to bypass the maybestates computations  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								becc43e1e1 
								
							
								 
							
						 
						
							
							
								
								added wokaround proposed by jklein to make the new sylvan version build on older osx  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								60ab1716b1 
								
							
								 
							
						 
						
							
							
								
								storm: bisimulation statistics  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e536851e53 
								
							
								 
							
						 
						
							
							
								
								Solver: provide information about solving method + number of iterations at INFO log level  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cb0d05c947 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								170105c261 
								
							
								 
							
						 
						
							
							
								
								Fixed "division by zero" error that occurred  when considering a CTMC with state rewards but without action rewards  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9425d3506e 
								
							
								 
							
						 
						
							
							
								
								reworked checking whether parameter lifting is applicable  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cf340bed52 
								
							
								 
							
						 
						
							
							
								
								cleaned up some utility functions  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								575210ae69 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d5d0a5f44a 
								
							
								 
							
						 
						
							
							
								
								fixed a few issues related to having CLN numbers as storm::RationalNumber  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9ba2f90483 
								
							
								 
							
						 
						
							
							
								
								started to implement a validation that checks whether parameter lifting is sound  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								36976f0607 
								
							
								 
							
						 
						
							
							
								
								temporarily fixed exact validation to make things compile again  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0464a248a4 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								48d5025bd9 
								
							
								 
							
						 
						
							
							
								
								Fixed checking of formulas whose subformulas contain an OperatorFormula (like nested OperatorFormulas or conjunctions of Operatorformulas).  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c5c14f3178 
								
							
								 
							
						 
						
							
							
								
								extended JSONExporter to properly export non-constant time/step intervals  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f0ae3a2dfb 
								
							
								 
							
						 
						
							
							
								
								Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cde59bd436 
								
							
								 
							
						 
						
							
							
								
								added Expression::evaluateAsRational  
							
							
								
 
							
							
						 
						9 years ago