e8fab0718c 
								
							
								 
							
						 
						
							
							
								
								fixed issues in division operations of sylvan for rational numbers and rational functions (division by zero not correctly handled)  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								44d582dc65 
								
							
								 
							
						 
						
							
							
								
								added more output about CArL when it's found on the system  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cebd3d252d 
								
							
								 
							
						 
						
							
							
								
								fixed include directory (cmake) for shipped carl  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								818bf8e447 
								
							
								 
							
						 
						
							
							
								
								added gurobi70 to FindGurobi.cmake  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								de2646b082 
								
							
								 
							
						 
						
							
							
								
								This commit fixes issue  #5  related to Gurobi not being linked properly when requested.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f5c327a10e 
								
							
								 
							
						 
						
							
							
								
								Boost must be set for shipped carl  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ea02ea0838 
								
							
								 
							
						 
						
							
							
								
								started overhaul of cli/api  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b76ee0210a 
								
							
								 
							
						 
						
							
							
								
								Fixed setting cmake flags for building shipped carl  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a9d6d80ef0 
								
							
								 
							
						 
						
							
							
								
								Warning in cmake if Z3 is not found  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0cdd32ff9f 
								
							
								 
							
						 
						
							
							
								
								added two test cases for the drn parser  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1ce122a0d6 
								
							
								 
							
						 
						
							
							
								
								fixed compile issue related to ambiguous call of operator<<  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								722e67fe64 
								
							
								 
							
						 
						
							
							
								
								parsing choice labels for explicit models  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								87f494627c 
								
							
								 
							
						 
						
							
							
								
								Fixes after carl update in order to get ginac from carl.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8f42bd2ec0 
								
							
								 
							
						 
						
							
							
								
								moved to new sparsepp version and made the appropriate changes  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ed2a1dc1de 
								
							
								 
							
						 
						
							
							
								
								CMake now ensures that carl is not only configured, but also built and thereby prevents compilation-time errors.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								920d48c2bd 
								
							
								 
							
						 
						
							
							
								
								storm config version now also correctly exported  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								92f04cdfa1 
								
							
								 
							
						 
						
							
							
								
								CppTemplate was not correctly listed as a dependency of storm.  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5f120fd5bb 
								
							
								 
							
						 
						
							
							
								
								Fixed enabling CLN when there is no system version of carl  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								28e91b8d0f 
								
							
								 
							
						 
						
							
							
								
								more work on symbolic bisimulation  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								03ad4c2783 
								
							
								 
							
						 
						
							
							
								
								first version of symbolic bisimulation minimization  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8c6b22bebc 
								
							
								 
							
						 
						
							
							
								
								Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1a9589dfa6 
								
							
								 
							
						 
						
							
							
								
								Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								86a783de92 
								
							
								 
							
						 
						
							
							
								
								two more fixes for issues pointed out by Tim: concurrency bug in sylvan and bug in symbolic quantitative check result  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4c99790213 
								
							
								 
							
						 
						
							
							
								
								Minor updates to ExprTk  
							
							
 
							
							
							Updated unknown symbol resolver interface to handle all types (scalar, string and vector)
Added compile-time check for vector indexing when using constant values
Added return statement enable/disable via parser settings
Added exprtk_disable_return_statement macro for disabling return statements and associated exceptions at the source code level. 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								977dd1ef53 
								
							
								 
							
						 
						
							
							
								
								Get GMP location from carl, set it as a hint for sylvan.  
							
							
								
 
							
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								8bfa699519 
								
							
								 
							
						 
						
							
							
								
								attempt to fix link error  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								187e8bc52b 
								
							
								 
							
						 
						
							
							
								
								fixed two bugs related to hybrid quantitative results  
							
							
								
 
							
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								becc43e1e1 
								
							
								 
							
						 
						
							
							
								
								added wokaround proposed by jklein to make the new sylvan version build on older osx  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								853b035473 
								
							
								 
							
						 
						
							
							
								
								fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)  
							
							
								
 
							
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								acd486f0f2 
								
							
								 
							
						 
						
							
							
								
								reverted a change in ExprTk: dots are no longer recognized as letters  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0354c9024a 
								
							
								 
							
						 
						
							
							
								
								moved to new sylvan version and made everything work again  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2e8ff870ff 
								
							
								 
							
						 
						
							
							
								
								completed interface of (sylvan) ADDs for storing rational functions  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c4dffe9a8b 
								
							
								 
							
						 
						
							
							
								
								tests for step bounded properties  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								24bc53549c 
								
							
								 
							
						 
						
							
							
								
								more tests on pmdps and fixes  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3f0afe9526 
								
							
								 
							
						 
						
							
							
								
								allowing underscore and dots as identifier symbols in exprtk  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b5e68b9914 
								
							
								 
							
						 
						
							
							
								
								fixes for z3LP solver and nativePolytopes  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								75130ab727 
								
							
								 
							
						 
						
							
							
								
								added patch by Joachim Klein that forwards the boost version storm found to carl  
							
							
								
 
							
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d15348ab80 
								
							
								 
							
						 
						
							
							
								
								Fixed problem with recompiling when using ninja  
							
							
								
 
							
							
						 
						9 years ago