c8e05f7137 
								
							
								 
							
						 
						
							
							
								
								Added explicit template instance.  
							
							
 
							
							
							Former-commit-id: 1ffcf0e47f 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d40573640f 
								
							
								 
							
						 
						
							
							
								
								Dropped our current Tarjan-implementation in favour of the path-based algorithm by Gabow (and others) as this seems to perform a lot better (at when comparing our implementations).  
							
							
 
							
							
							Former-commit-id: 5cfeb85193 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0c305825f3 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into philippTopologicalRevival  
							
							
 
							
							
							Conflicts:
	src/counterexamples/PathBasedSubsystemGenerator.h
Former-commit-id: 106eed626b 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								59ca5fcdba 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into philippTopologicalRevival  
							
							
 
							
							
							Conflicts:
	src/counterexamples/PathBasedSubsystemGenerator.h
	src/storm.cpp
Former-commit-id: 338637dcd6 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								493f93a94b 
								
							
								 
							
						 
						
							
							
								
								Added __restrict__ keyword to CUDA kernel. This should enhance compiler optimization.  
							
							
 
							
							
							Refactored TopologicalValueIterationNondeterministicLinearEquationSolver to support "down-casting" to float.
Added better timing output.
Former-commit-id: 688c40decb 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4f25312a6b 
								
							
								 
							
						 
						
							
							
								
								Adapted SMT-based counterexample generator such that it works with the new property classes.  
							
							
 
							
							
							Former-commit-id: 359a4c706f 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7f7ddc06e1 
								
							
								 
							
						 
						
							
							
								
								Removed two erronous keywords.  
							
							
 
							
							
							Former-commit-id: ecc36e0b07 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5a0059d110 
								
							
								 
							
						 
						
							
							
								
								Commented out the SMTMinimalCommandSetGeneraator, again.  
							
							
 
							
							
							Former-commit-id: 4e0427caaf 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4f5b0b5949 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'refactorFormulas'  
							
							
 
							
							
							Conflicts:
	src/counterexamples/SMTMinimalCommandSetGenerator.h
	src/storm.cpp
Former-commit-id: f65836b10d 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								52cfe9f02d 
								
							
								 
							
						 
						
							
							
								
								Fixed some compile errors.  
							
							
 
							
							
							- Added a missing inlude (boost/functional/hash.hpp) to SparseMatrix.h. I don't know how this could have been compiled without.
- Changed a return type in the stub section of the GurobiLpSolver to void. Not correctly overwrites the base class function.
- Went through the change history of the SparseMarkovAutomatonCslModelchecker.h to correctly integrate all changes made in this branch with the changes of the other branches.
Former-commit-id: 43ce12274b 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b84ef7bebc 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into refactorFormulas  
							
							
 
							
							
							Conflicts:
	src/counterexamples/MILPMinimalLabelSetGenerator.h
	src/counterexamples/PathBasedSubsystemGenerator.h
	src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
	src/parser/PrctlParser.cpp
	src/storm.cpp
	test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
	test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
All conflicts resoved. Revision of src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h pending.
Former-commit-id: 6bf9d05dba 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d75e32b83e 
								
							
								 
							
						 
						
							
							
								
								Renames the folder formula to properties and the namespace property to properties.  
							
							
 
							
							
							Former-commit-id: 236ed22c7d 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6b2b1e4d7b 
								
							
								 
							
						 
						
							
							
								
								Finished the documentation of the formulas.  
							
							
 
							
							
							- Also removed one superflous class (IOptimizingOperator).
- Killed all warnings concerning missing virtual destructor in the interfaced for the modelchecker.
- A whole lot of little things I can't quite remember.
Next up: Remerge
Former-commit-id: 28fedd036c 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								71320239f1 
								
							
								 
							
						 
						
							
							
								
								Some debug output.  
							
							
 
							
							
							Former-commit-id: dd0a60f099 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								cbf1301e47 
								
							
								 
							
						 
						
							
							
								
								Small bugfix.  
							
							
 
							
							
							Former-commit-id: 11d4a2474a 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7f15f358c1 
								
							
								 
							
						 
						
							
							
								
								Removed the FormulaCheckers.  
							
							
 
							
							
							Former-commit-id: 24910974c6 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								57882db84e 
								
							
								 
							
						 
						
							
							
								
								Fixed warnings about unused variables in PathBasedSubsystemGenerator and SMTMinimalCommandSetGenerator. Also some stuff with type conversions.  
							
							
 
							
							
							Fixed the missing include/definition for getcwd
Former-commit-id: 08f82f2ed2 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								40a8fdd6e4 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'refactorFormulas' of  https://sselab.de/lab9/private/git/storm  into refactorFormulas  
							
							
 
							
							
							Former-commit-id: 9fc5309029 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0a2a759932 
								
							
								 
							
						 
						
							
							
								
								Ltl testng.  
							
							
 
							
							
							Former-commit-id: 57f486db59 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a49991484c 
								
							
								 
							
						 
						
							
							
								
								Fixed missing definitions for the current working directory.  
							
							
 
							
							
							Former-commit-id: cc99143526 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3bc31e927d 
								
							
								 
							
						 
						
							
							
								
								Added per-formula timing output.  
							
							
 
							
							
							This is basically a picky merge from my CUDA branch.
Former-commit-id: bb386486bb 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								94b2d45e05 
								
							
								 
							
						 
						
							
							
								
								Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp.  
							
							
 
							
							
							Former-commit-id: 155d96a54f 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								422a317407 
								
							
								 
							
						 
						
							
							
								
								Made the OptimalSCC algorithm MUCH faster.  
							
							
 
							
							
							Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp.
Former-commit-id: 77ba352a29 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4614eccccb 
								
							
								 
							
						 
						
							
							
								
								Addendum to last commit: Forgot the files for the csl filter test.  
							
							
 
							
							
							Former-commit-id: cb38349e80 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								a39e9a821f 
								
							
								 
							
						 
						
							
							
								
								Fixed a type error in TBB implementation.  
							
							
 
							
							
							Former-commit-id: 680f43b36a 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7e77fbb6bb 
								
							
								 
							
						 
						
							
							
								
								Some testing stuff.  
							
							
 
							
							
							Former-commit-id: d7a9085af5 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4a1358fb79 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  into philippTopologicalRevival  
							
							
 
							
							
							Former-commit-id: af74c0e14d 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								67cd9e58ba 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  into philippTopologicalRevival  
							
							
 
							
							
							Former-commit-id: ff3bcbc189 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4ba45efd1c 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'parametricSystems' of  https://sselab.de/lab9/private/git/storm  into parametricSystems  
							
							
 
							
							
							Former-commit-id: b022b59c61 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ff572c7f6f 
								
							
								 
							
						 
						
							
							
								
								Sped up PRISM parser by letting it skip the actual command definitions in the first run (because only gathering constants, variables and formulas is important in this particular run).  
							
							
 
							
							
							Former-commit-id: 0b25c73fa4 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f485974187 
								
							
								 
							
						 
						
							
							
								
								Fixed (asynch) leader election to comply with our grammar. Added LOG_DEBUG macro.  
							
							
 
							
							
							Former-commit-id: 7b22ecba8e 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1c4d7b9ef9 
								
							
								 
							
						 
						
							
							
								
								Some more testing.  
							
							
 
							
							
							Former-commit-id: 3105a0bf3b 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								577e48f8bf 
								
							
								 
							
						 
						
							
							
								
								Bugfix for the dimensions of some data of parsed Markov automata.  
							
							
 
							
							
							Former-commit-id: ab11be9ec4 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								952747a9bc 
								
							
								 
							
						 
						
							
							
								
								Modified some rules in the expression parser such that less redundant parsing is done.  
							
							
 
							
							
							Former-commit-id: aa072c9f9b 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								5bb76eb12e 
								
							
								 
							
						 
						
							
							
								
								Bugfix for storm::utility::vector::reduceVector to correctly compute which choices were taken to achieve extremal values.  
							
							
 
							
							
							Former-commit-id: c200835cf5 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e2c2177dca 
								
							
								 
							
						 
						
							
							
								
								Adapted MaxSAT-based minimal command set generator to some recent changes to make it work again.  
							
							
 
							
							
							Former-commit-id: 8f8c33b920 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								3887cb57aa 
								
							
								 
							
						 
						
							
							
								
								Fix for temporaries and non const references  
							
							
 
							
							
							Former-commit-id: 4eadf6cdab 
							
						 
						11 years ago