dc1aea83ed 
								
							
								 
							
						 
						
							
							
								
								Added --trace and logging in general to functional tests.  
							
							
 
							
							
							Former-commit-id: a4cef18e6c 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1985c708ea 
								
							
								 
							
						 
						
							
							
								
								Revert back to older version  ae0e423a4e [formerly  e3f9d7a533]  
							
							
 
							
							
							Former-commit-id: 9f72a10358 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bdf415d416 
								
							
								 
							
						 
						
							
							
								
								Added fancy tests.  
							
							
 
							
							
							Former-commit-id: 0960553112 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bd36c7a2e6 
								
							
								 
							
						 
						
							
							
								
								Finally, some progress.  
							
							
 
							
							
							Former-commit-id: 2eb5173abc 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								156ab071a5 
								
							
								 
							
						 
						
							
							
								
								more work on abstraction refinement  
							
							
 
							
							
							Former-commit-id: 20dcaa7518 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d76e9729da 
								
							
								 
							
						 
						
							
							
								
								Leave Replacement finally working.  
							
							
 
							
							
							Former-commit-id: 239ea6d897 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bc1eff959f 
								
							
								 
							
						 
						
							
							
								
								graph algorithms for games now also compute player 2 prob0/1 states and the generated strategies are adapted accordingly  
							
							
 
							
							
							Former-commit-id: da52581328 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c9f2eef826 
								
							
								 
							
						 
						
							
							
								
								Added functionality for replacing leaves in SRF MTBDDs.  
							
							
 
							
							
							Former-commit-id: d7af779036 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d3c492124a 
								
							
								 
							
						 
						
							
							
								
								Fixed min/max Abstract w. repr.  
							
							
 
							
							
							Finally.
Former-commit-id: 1ccc06d924 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								375ea1b194 
								
							
								 
							
						 
						
							
							
								
								fixed bug in cudd minAbstractRepresentative, adapted tests, passing now  
							
							
 
							
							
							Former-commit-id: 7f45376343 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								da199866e6 
								
							
								 
							
						 
						
							
							
								
								Added tests for minAbstractRepresentative.  
							
							
 
							
							
							Everything still in early alpha. Expect Debug output.
Former-commit-id: 2712fce4dd 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bde84d0073 
								
							
								 
							
						 
						
							
							
								
								fixed symbolic game solver wrt. illegal masks. numerical solving step in game-based model checker working, but no refinement yet.  
							
							
 
							
							
							Former-commit-id: 6189a1e538 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								73a3461650 
								
							
								 
							
						 
						
							
							
								
								Fixed CUDD and Sylvan existsRepresentative.  
							
							
 
							
							
							Former-commit-id: e3ec69ab37 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c184f6a541 
								
							
								 
							
						 
						
							
							
								
								Worked on Sylvan min/max ADD abstract w. representative.  
							
							
 
							
							
							More tests for existsRepr.
Former-commit-id: 08c5d6e9bb 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7d50a6b839 
								
							
								 
							
						 
						
							
							
								
								graph algorithms for games can now produce player strategies even if they can pick any choice (if requested)  
							
							
 
							
							
							Former-commit-id: 98119f274d 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b5aa778c51 
								
							
								 
							
						 
						
							
							
								
								Fixed PrismMenuGameTest.  
							
							
 
							
							
							Former-commit-id: edce18058a 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e45b3d2940 
								
							
								 
							
						 
						
							
							
								
								Fixed Sylvan implementation of existsAbstractRepresentative.  
							
							
 
							
							
							Added more tests.
Former-commit-id: 6a4003bb5e 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								61c227d6f8 
								
							
								 
							
						 
						
							
							
								
								Added a test for reporting a buggy bug.  
							
							
 
							
							
							Former-commit-id: aace547656 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5bf666be4c 
								
							
								 
							
						 
						
							
							
								
								fix in existsAbstractRepresentative  
							
							
 
							
							
							Former-commit-id: c884deaf11 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9878c1bdc3 
								
							
								 
							
						 
						
							
							
								
								fixed some tests that were failing because of (now) proper bottom state computation  
							
							
 
							
							
							Former-commit-id: ecc8dfb065 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								be7353358f 
								
							
								 
							
						 
						
							
							
								
								Added Test for constants in Cudd/Sylvan.  
							
							
 
							
							
							Added functionality for existsAbstractRepresentative in Sylvan. Still very broken!
Former-commit-id: df2b36a8d8 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9e64e998f3 
								
							
								 
							
						 
						
							
							
								
								fixed tests wrt. proper bottom state computation  
							
							
 
							
							
							Former-commit-id: 223795c955 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1be735ec1b 
								
							
								 
							
						 
						
							
							
								
								fixed tests in response to 'fixing' flattenModules  
							
							
 
							
							
							Former-commit-id: 07f28fb20a 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b3e77730a9 
								
							
								 
							
						 
						
							
							
								
								added uniqueness mechanism in flattenModules to compensate for missing uniqueness in allsat of solvers  
							
							
 
							
							
							Former-commit-id: b4ebd17f68 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b14f866e01 
								
							
								 
							
						 
						
							
							
								
								added more flatten tests  
							
							
 
							
							
							Former-commit-id: 7e35a90c88 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3e9f9552b1 
								
							
								 
							
						 
						
							
							
								
								fixed tests: using shared_ptr instead of unique_ptr for SMT solver factory in abstraction  
							
							
 
							
							
							Former-commit-id: 6159a20565 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								81311690ab 
								
							
								 
							
						 
						
							
							
								
								Fixed errors because of changed API.  
							
							
 
							
							
							Former-commit-id: 7f771dc576 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4fff7b39ef 
								
							
								 
							
						 
						
							
							
								
								Added template instanziation for storm::RationalFunction.  
							
							
 
							
							
							Added a test for Prism AbstractPrograms with storm::RationalFunction.
Former-commit-id: 5a696149cb 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ba81925c1d 
								
							
								 
							
						 
						
							
							
								
								renamed smt2smtsolver to smtlibsmtsolver and cleaned make files  
							
							
 
							
							
							Former-commit-id: 78c74dc9a5 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								19bf801456 
								
							
								 
							
						 
						
							
							
								
								Fixed MDP tests  
							
							
 
							
							
							Former-commit-id: 058bcbc4c6 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d97b0b2897 
								
							
								 
							
						 
						
							
							
								
								cleaned tests  
							
							
 
							
							
							Former-commit-id: 8d376e3c75 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b6465020a2 
								
							
								 
							
						 
						
							
							
								
								towards working tests in pla  
							
							
 
							
							
							Former-commit-id: 3542f8a1d0 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0717ffe053 
								
							
								 
							
						 
						
							
							
								
								Added AND_EXISTS to sylvan+RationalFunction  
							
							
 
							
							
							Former-commit-id: 7b462145cf 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2637d51afc 
								
							
								 
							
						 
						
							
							
								
								set formula  
							
							
 
							
							
							Former-commit-id: e5d9a4ca30 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9632ca9f6f 
								
							
								 
							
						 
						
							
							
								
								fixed tests  
							
							
 
							
							
							Former-commit-id: c14b7234e2 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0ef2b55c75 
								
							
								 
							
						 
						
							
							
								
								made some region settings attribute to the model checker instead of global  
							
							
 
							
							
							Former-commit-id: e53ca96760 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								548ba8bbeb 
								
							
								 
							
						 
						
							
							
								
								somehow managed my way through the policy guessing, several minor extensions to solvers  
							
							
 
							
							
							Former-commit-id: c4bb6453e7 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								18b0f07581 
								
							
								 
							
						 
						
							
							
								
								tweaked Bdd toExpression a bit to be more versatile  
							
							
 
							
							
							Former-commit-id: 858948f1b7 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								52577e2740 
								
							
								 
							
						 
						
							
							
								
								added game abstraction tests for sylvan and made them work (in particular implemented toExpression for sylvan BDDs)  
							
							
 
							
							
							Former-commit-id: 8fdc34cb55 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4999cfa8a0 
								
							
								 
							
						 
						
							
							
								
								By performance tests, you served us well but we do not love you any longer  
							
							
 
							
							
							Former-commit-id: 048c3447cb 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d8d8f70f0c 
								
							
								 
							
						 
						
							
							
								
								functional tests now work with the refactored code base  
							
							
 
							
							
							Former-commit-id: 2d7d7e111a 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								53f83c9214 
								
							
								 
							
						 
						
							
							
								
								moved menu-game abstraction to separate folder and made everything compile again  
							
							
 
							
							
							Former-commit-id: a833ca1152 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								58eb54926c 
								
							
								 
							
						 
						
							
							
								
								Fixed Sylvan bugs.  
							
							
 
							
							
							Added a lot of debugging options and output, controlled by #define's.
Added more template specializations for storm::RationalFunction.
Former-commit-id: 416c32d196 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5b8cf447c7 
								
							
								 
							
						 
						
							
							
								
								Small changes in tests to compile without Carl  
							
							
 
							
							
							Former-commit-id: 6ec191ce0a 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								291f120cc0 
								
							
								 
							
						 
						
							
							
								
								Added the encoding and identity test for Rational Functions.  
							
							
 
							
							
							Former-commit-id: ed9695a5e2 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								07d4848f55 
								
							
								 
							
						 
						
							
							
								
								Fixed missing include in InternalSylvanAdd.cpp  
							
							
 
							
							
							Added simple test for Sylvan + RationalFunctions.
Former-commit-id: ffb747a861 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f681206393 
								
							
								 
							
						 
						
							
							
								
								building markov automata from prism code  
							
							
 
							
							
							Former-commit-id: 791c49c7cf 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0f84cdcadb 
								
							
								 
							
						 
						
							
							
								
								Fixed performance tests.  
							
							
 
							
							
							WARNING: I had to remove the SolverSelection in the call due to the new API - the performance tests might now all use the same Solver.
Former-commit-id: 7d5ed3191d 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								83c4b1647c 
								
							
								 
							
						 
						
							
							
								
								solvers now can allocated auxiliary memory  
							
							
 
							
							
							Former-commit-id: 76dc1a1679 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								95b95d9c64 
								
							
								 
							
						 
						
							
							
								
								fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact  
							
							
 
							
							
							Former-commit-id: de103e19ad 
							
						 
						9 years ago