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  
				
					
						
							
							
								 
						
							
							
							
								
							
								2f3b090a51 
								
							
								 
							
						 
						
							
							
								
								Merge remote-tracking branch 'origin/master' into symbolic_state_elimination  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								853b035473 
								
							
								 
							
						 
						
							
							
								
								fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ee510df4ec 
								
							
								 
							
						 
						
							
							
								
								add Path stream print for debug / Python __str__  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3a09a378fc 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactor_pla  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								457943351d 
								
							
								 
							
						 
						
							
							
								
								fixed matrix building in ModelInstantiator for deterministic models. Previously, a non-trivial row grouping was introduced.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dd40254628 
								
							
								 
							
						 
						
							
							
								
								PLA for continuous models  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b811ebcf88 
								
							
								 
							
						 
						
							
							
								
								dd-based policy iteration appears to be working  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f6e194592f 
								
							
								 
							
						 
						
							
							
								
								remove always building sylvan  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0135793c44 
								
							
								 
							
						 
						
							
							
								
								update to newest sylvan version  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								153339c5be 
								
							
								 
							
						 
						
							
							
								
								first draft of policy iteration using DDs  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								952776a057 
								
							
								 
							
						 
						
							
							
								
								hybrid engine working for rational numbers  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ee90c51b2a 
								
							
								 
							
						 
						
							
							
								
								cleaned up constants.cpp to finalize separation of rational functions and rational numbers  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								aaa6f13cf4 
								
							
								 
							
						 
						
							
							
								
								separated rational numbers and rational functions and added support for rational numbers to sylvan  
							
							
								
 
							
							
						 
						9 years ago