6eb415f87f 
								
							
								 
							
						 
						
							
							
								
								Tests for MathSAT now run through on Mac OS.  
							
							
 
							
							
							Former-commit-id: 9f6cf0af6a 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d8be64f0d7 
								
							
								 
							
						 
						
							
							
								
								Started on making MathSatSmtSolver work properly.  
							
							
 
							
							
							Former-commit-id: c370658b26 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7014d289e8 
								
							
								 
							
						 
						
							
							
								
								Fixed some issues related to bisimulation in the presence of state rewards.  
							
							
 
							
							
							Former-commit-id: 7f26a7bcf9 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7644a74fcd 
								
							
								 
							
						 
						
							
							
								
								Removed some superfluous lines in test.  
							
							
 
							
							
							Former-commit-id: 2c2bd0ba67 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								370a0ae476 
								
							
								 
							
						 
						
							
							
								
								Fixed some issues in bisimulation and added some tests.  
							
							
 
							
							
							Former-commit-id: 98801de9db 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1a4d4fd5a7 
								
							
								 
							
						 
						
							
							
								
								Added a test I used for finding the SCC Bug.  
							
							
 
							
							
							Former-commit-id: 5936e79d04 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								433bae1156 
								
							
								 
							
						 
						
							
							
								
								Switched from an option to fix deadlocks to an option to not fix the deadlocks. Hence, deadlocks are now fixed by default unless otherwise requested.  
							
							
 
							
							
							Former-commit-id: 9434215807 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								51becda4b3 
								
							
								 
							
						 
						
							
							
								
								Commit to switch workplace.  
							
							
 
							
							
							Former-commit-id: da5fac08cf 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5ecc96fa3a 
								
							
								 
							
						 
						
							
							
								
								Fixed some more places in the code to use the new option system.  
							
							
 
							
							
							Former-commit-id: 15ff64f1dc 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a995d7dd4a 
								
							
								 
							
						 
						
							
							
								
								The tests now run fine with the new option system.  
							
							
 
							
							
							Former-commit-id: 6d6c510131 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								266d660d89 
								
							
								 
							
						 
						
							
							
								
								Added functions responsible for printing the help. Started adapting the tests to the new option system.  
							
							
 
							
							
							Former-commit-id: 0407d8223e 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5817fe50b6 
								
							
								 
							
						 
						
							
							
								
								post merge fixes  
							
							
 
							
							
							Former-commit-id: 2f9bc01abd 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9ad12616e2 
								
							
								 
							
						 
						
							
							
								
								Renamed files in settings module a bit. Started on the pseudo-modular module-settings.  
							
							
 
							
							
							Former-commit-id: b3162aa86b 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								96e1f8faf9 
								
							
								 
							
						 
						
							
							
								
								Renamed Settings class to SettingsManager.  
							
							
 
							
							
							Former-commit-id: 2b33f4c8d0 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9569426c86 
								
							
								 
							
						 
						
							
							
								
								Moved option registration to the settings class (so it's not deceentralized any longer). This enables to build storm as a library and on top of that build some exectuables, which saves a lot of compile time as soon as several targets have to be built or one switches between targets.  
							
							
 
							
							
							Former-commit-id: 69e0d526c7 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1cc930f0e4 
								
							
								 
							
						 
						
							
							
								
								Added proper source grouping for properties directory. Fixed one performance tests. Started on SCC-based reachability model checker.  
							
							
 
							
							
							Former-commit-id: e48c163783 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								552b3eaab7 
								
							
								 
							
						 
						
							
							
								
								Fixed SCC performance tests.  
							
							
 
							
							
							Former-commit-id: a6b46e2fc5 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								59dbc5a71e 
								
							
								 
							
						 
						
							
							
								
								Fixed tests to comply with new requirement for hint in tra-file (needs to be at the very beginning, no prior white spaces).  
							
							
 
							
							
							Former-commit-id: 60bfb720b8 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								fff4e61fc3 
								
							
								 
							
						 
						
							
							
								
								Changed interface of matrix builder slightly to be able to also not force the resulting matrix to certain dimensions, but merely to reserve the desired space.  
							
							
 
							
							
							Former-commit-id: e36d05398e 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ac420f13d0 
								
							
								 
							
						 
						
							
							
								
								Fixed some warnings in various places.  
							
							
 
							
							
							Former-commit-id: fbfbfc2bcb 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ab58103555 
								
							
								 
							
						 
						
							
							
								
								Started to pimp matrix. First step: added proper methods setColumn/setValue that operate on a matrix entry and removed the non-const versions of getColumn/getValue. Added a typedef for the index type in the matrix so that it becomes possible to have matrices with a different index type (e.g. 32-bit values).  
							
							
 
							
							
							Former-commit-id: 3cc0fdf9ee 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7f7ddc06e1 
								
							
								 
							
						 
						
							
							
								
								Removed two erronous keywords.  
							
							
 
							
							
							Former-commit-id: ecc36e0b07 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d75e32b83e 
								
							
								 
							
						 
						
							
							
								
								Renames the folder formula to properties and the namespace property to properties.  
							
							
 
							
							
							Former-commit-id: 236ed22c7d 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ea427fcde1 
								
							
								 
							
						 
						
							
							
								
								Fixed include directories for CUDA Plugin in CMakeLists.txt  
							
							
 
							
							
							Refactored all code related to the SPMV kernels to work with float.
Wrote a test that determines whether the compiler uses 64bit boundary alignments on std::pairs of uint64 and float.
Introduced functions that allow for conversions between different ValueTypes (e.g. from float to double and backwards).
Former-commit-id: 830d24064f 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								532b0cf3ad 
								
							
								 
							
						 
						
							
							
								
								Added function to test if a formula is a probability bounded reachability formula, i.e. conforms to the pattern P[<,<=,>,>=]p ([phi U, E] psi) where phi, psi are propositional formulas (consisting only of And, Or, Not and AP).  
							
							
 
							
							
							- For that implemented function that checks if a formula is a propositional logic formula to all three logics.
- Added tests for the function.
- Added documentation for the function.
Former-commit-id: 3fcb84b990 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								27df78c2b0 
								
							
								 
							
						 
						
							
							
								
								Finished testing Ltl.  
							
							
 
							
							
							- Regrettably, the LtlFilterTest could not be done, since an Ltl modechecker would be needed for that. Which, we don't have.
|- So that is a TODO until such a modelchecker is implemented.
- This concludes the testing for the refactured formulas.
Next up: Documentation.
Former-commit-id: 2d731edcd9 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0a2a759932 
								
							
								 
							
						 
						
							
							
								
								Ltl testng.  
							
							
 
							
							
							Former-commit-id: 57f486db59 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2687809591 
								
							
								 
							
						 
						
							
							
								
								Finished testing of Csl.  
							
							
 
							
							
							Former-commit-id: 91172a1b89 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								33386f4c5f 
								
							
								 
							
						 
						
							
							
								
								Changed the actions in the filters to be shared_ptr instead of raw pointers. This prevents memory leaks when a filter is destructed.  
							
							
 
							
							
							- Also handled nullptr actions.
|- They are checked for in the constructor as well as in the add method and filtered out. No segfaults do to nullptr actions anymore.
Former-commit-id: 84b3b2a978 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b7357c2cf9 
								
							
								 
							
						 
						
							
							
								
								Testing, noticed that vectors of pointers are not good. Changing that.  
							
							
 
							
							
							Former-commit-id: 460854c49c 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								73ddba5b29 
								
							
								 
							
						 
						
							
							
								
								Merged master, applied fixes.  
							
							
 
							
							
							Added feedback from the cuda plugin and return of iteration count.
Former-commit-id: 711ca3d9ec 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1c4d7b9ef9 
								
							
								 
							
						 
						
							
							
								
								Some more testing.  
							
							
 
							
							
							Former-commit-id: 3105a0bf3b 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								93a08538e3 
								
							
								 
							
						 
						
							
							
								
								Reverted debug change in test.  
							
							
 
							
							
							Former-commit-id: efeacaf595 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7c5603de3e 
								
							
								 
							
						 
						
							
							
								
								Improved performance of the expression parser a bit more.  
							
							
 
							
							
							Former-commit-id: 7a0ae116c9 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								aecd0e3cb8 
								
							
								 
							
						 
						
							
							
								
								Made Storm compile again without Z3: guarded some header inclusions and function definitions/implementations. Also guarded the tests that require certain libraries (like Gurobi, glpk, Z3), so that tests do not fail any more when the libraries are not available.  
							
							
 
							
							
							Former-commit-id: 307036e25c 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2c59dd6f32 
								
							
								 
							
						 
						
							
							
								
								Finished unit tests for the actions.  
							
							
 
							
							
							Next up: Update the parser tests.
Former-commit-id: c0db7bd1d4 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ee1ebdf91d 
								
							
								 
							
						 
						
							
							
								
								Removed the visitor from LTL and refactured the formulas to use shared pointer in stead of standart pointer.  
							
							
 
							
							
							Next up: Continue testing.
Former-commit-id: 0103895e13 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								40c698af90 
								
							
								 
							
						 
						
							
							
								
								Some fixes to make new SMT framework compile with clang under Mac OS (includes fixes to some initializiation ordering warnings). Bugfix for PRISM parser to correctly handle formulas.  
							
							
 
							
							
							Former-commit-id: d513476066 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								52d3d91060 
								
							
								 
							
						 
						
							
							
								
								Implemented Unsat Core/Assumtions & simple test  
							
							
 
							
							
							Former-commit-id: f79ee3a809 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d2f4c85711 
								
							
								 
							
						 
						
							
							
								
								Made changes to comply with new SparseMatrix Interface (YUCK).  
							
							
 
							
							
							Fixed tests, all that stuff.
Former-commit-id: c78de5f8ce 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9fe246a98b 
								
							
								 
							
						 
						
							
							
								
								Renamed the folders containing the formulas to lowercase to adhere to the naming conventions and Started with testing.  
							
							
 
							
							
							-Tests for BoundAction done
Former-commit-id: d5698d3d53 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a815a6f425 
								
							
								 
							
						 
						
							
							
								
								Implemented allSat with z3 and test  
							
							
 
							
							
							Former-commit-id: 3795fc00c2 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								93c03fff3f 
								
							
								 
							
						 
						
							
							
								
								Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation  
							
							
 
							
							
							Former-commit-id: ca5f876655 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								caf96c04e0 
								
							
								 
							
						 
						
							
							
								
								Extended DD interface by methods to generate explicit row-grouped matrices from DDs.  
							
							
 
							
							
							Former-commit-id: 1945d7be6d 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8587f68eb1 
								
							
								 
							
						 
						
							
							
								
								Fixed toMatrix conversion using ODDs. The next step is to generate non-deterministic matrices, i.e., matrices with row groups.  
							
							
 
							
							
							Former-commit-id: e4a9c5f0ed 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								236e7fa290 
								
							
								 
							
						 
						
							
							
								
								Another step towards generating explicit data structures from DDs using ODDs.  
							
							
 
							
							
							Former-commit-id: 5b7e3e8680 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f12ff82baf 
								
							
								 
							
						 
						
							
							
								
								Added getNodeCount for ODD and fixed a bug concerning boolean meta variables.  
							
							
 
							
							
							Former-commit-id: 79eb69226b 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5d53c6efa5 
								
							
								 
							
						 
						
							
							
								
								Added ODD-concept to easily convert between DD-based and explicit formats.  
							
							
 
							
							
							Former-commit-id: f2a2a002b7 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								72cc5f2188 
								
							
								 
							
						 
						
							
							
								
								Added 'power' as a binary operator in expression classes and expression grammar.  
							
							
 
							
							
							Former-commit-id: c58321709e 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								03399375f8 
								
							
								 
							
						 
						
							
							
								
								Fixed an unintended 32bit shift being expanded to 64 bit  
							
							
 
							
							
							Former-commit-id: b2adc2a5ba 
							
						 
						12 years ago