2a7dc0fad0 
								
							
								 
							
						 
						
							
							
								
								renamed MarkovChainSettings  
							
							
 
							
							
							Former-commit-id: 39024731f8 
							
						 
						9 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3b5c27acba 
								
							
								 
							
						 
						
							
							
								
								more test-files included, two small fixes in parser  
							
							
 
							
							
							Former-commit-id: 0e9000c988 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b64dc408ac 
								
							
								 
							
						 
						
							
							
								
								test case for die.jani parsing  
							
							
 
							
							
							Former-commit-id: b58a9102a6 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a0d659f2da 
								
							
								 
							
						 
						
							
							
								
								always use shared_ptr<Formula const>  
							
							
 
							
							
							Former-commit-id: 63a447e887 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								37220cae57 
								
							
								 
							
						 
						
							
							
								
								removed two assertions in tests because they no longer apply  
							
							
 
							
							
							Former-commit-id: fcf132e685 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								effadc5cca 
								
							
								 
							
						 
						
							
							
								
								Split into general settings and markov chain settings  
							
							
 
							
							
							Former-commit-id: 619a2e3622 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dc8a5b11e0 
								
							
								 
							
						 
						
							
							
								
								more refactoring regarding fragment checking  
							
							
 
							
							
							Former-commit-id: fd335f6f8e 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d8191d8c6a 
								
							
								 
							
						 
						
							
							
								
								const formulae  
							
							
 
							
							
							Former-commit-id: 910d7ca539 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								27e06940a9 
								
							
								 
							
						 
						
							
							
								
								templated all explicit parsers so that they may now be modified to produce non-double models  
							
							
 
							
							
							Former-commit-id: dd7f8767f8 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f9f5a4e206 
								
							
								 
							
						 
						
							
							
								
								reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas  
							
							
 
							
							
							Former-commit-id: a2849d6534 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b3178e17f6 
								
							
								 
							
						 
						
							
							
								
								more bug fixes  
							
							
 
							
							
							Former-commit-id: 0b33b30efa 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dbc7d860a4 
								
							
								 
							
						 
						
							
							
								
								functional tests compile again, started to debug changes  
							
							
 
							
							
							Former-commit-id: efef0e6487 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f85d28325e 
								
							
								 
							
						 
						
							
							
								
								Further work towards faster and more modular compilation  
							
							
 
							
							
							Former-commit-id: 9de50910b8 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3c2040f4b7 
								
							
								 
							
						 
						
							
							
								
								Removed many superfluous includes, added some source files -- towards faster compilation  
							
							
 
							
							
							Former-commit-id: a575a97d40 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								56b4f53ce7 
								
							
								 
							
						 
						
							
							
								
								got rid of more warnings  
							
							
 
							
							
							Former-commit-id: 5c39f63c69 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e338cbe069 
								
							
								 
							
						 
						
							
							
								
								fixed a lot of warnings in the tests  
							
							
 
							
							
							Former-commit-id: b6752202ac 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d62539165e 
								
							
								 
							
						 
						
							
							
								
								'Identity updates' can now be described as applying 'true' in PRISM programs.  
							
							
 
							
							
							Former-commit-id: b2f70eb465 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9d5c3e7e2f 
								
							
								 
							
						 
						
							
							
								
								added functionality to flatten the modules of a PRISM program into one module  
							
							
 
							
							
							Former-commit-id: 04faac9c67 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a1dae8849e 
								
							
								 
							
						 
						
							
							
								
								Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented.  
							
							
 
							
							
							Former-commit-id: d4e6df30b5 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e79233bd7b 
								
							
								 
							
						 
						
							
							
								
								Added check in PRISM program that prevents global varibles from written in possibly synchronizing commands.  
							
							
 
							
							
							Former-commit-id: 34e34cacbe 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								89df9621a9 
								
							
								 
							
						 
						
							
							
								
								MDP model checker works again.  
							
							
 
							
							
							Former-commit-id: 2c24da6192 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9026aa9ac9 
								
							
								 
							
						 
						
							
							
								
								Adapted first model checker to the new properties.  
							
							
 
							
							
							Former-commit-id: 206d6c9858 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f673dccd76 
								
							
								 
							
						 
						
							
							
								
								Formula parser works again. Tests adapted.  
							
							
 
							
							
							Former-commit-id: 78ce54d69f 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1699732dce 
								
							
								 
							
						 
						
							
							
								
								More work on logic classes.  
							
							
 
							
							
							Former-commit-id: 9d94e02b74 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								aaefe7dfa5 
								
							
								 
							
						 
						
							
							
								
								Fixed some tests/parser.  
							
							
 
							
							
							Former-commit-id: d1767861c4 
							
						 
						11 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8e71081f1e 
								
							
								 
							
						 
						
							
							
								
								Functional tests now work again.  
							
							
 
							
							
							Former-commit-id: 46d964ad22 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								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  
				
					
						
							
							
								 
						
							
							
							
								
							
								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  
				
					
						
							
							
								 
						
							
							
							
								
							
								d75e32b83e 
								
							
								 
							
						 
						
							
							
								
								Renames the folder formula to properties and the namespace property to properties.  
							
							
 
							
							
							Former-commit-id: 236ed22c7d 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								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  
				
					
						
							
							
								 
						
							
							
							
								
							
								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  
				
					
						
							
							
								 
						
							
							
							
								
							
								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 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								72cc5f2188 
								
							
								 
							
						 
						
							
							
								
								Added 'power' as a binary operator in expression classes and expression grammar.  
							
							
 
							
							
							Former-commit-id: c58321709e 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9a28e5b580 
								
							
								 
							
						 
						
							
							
								
								Added proper formula string method to filters.  
							
							
 
							
							
							- Lots of debugging
- Changed the way the filter keeps information about the scheduler to use for probability/reward queries.
| This was done by keeping a special action at the first position of the action list.
| Which was not exactly consistent with the idea behind the filter actions.
| Now the filter keeps this information as an enum value in a member variable.
- All but one tests are green. So we almost reestablished full functionality.
|- The last test that still fails is SparseMdpPrctlModelCheckerTest.Dice where the second to last model check returns the wrong result.
Next up: Debug. Then introduce the full range of filter actions.
Former-commit-id: fd311966cc 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4bf0299279 
								
							
								 
							
						 
						
							
							
								
								Changed the Prctl/Csl formula parsers to be static classes.  
							
							
 
							
							
							- Also fixed up control flow and some tests for new interfaces.
|-> It now compiles again.
Next up: More functionallity in the filter.
Former-commit-id: 21d43e75c4 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								db232fe39b 
								
							
								 
							
						 
						
							
							
								
								Moved from pair to MatrixEntry as the basic building block of the matrix. Now matrix elements can be accessed in a more readable way.  
							
							
 
							
							
							Former-commit-id: f6514eb0cd 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								92ee6187fa 
								
							
								 
							
						 
						
							
							
								
								Added more query methods to expressions. SparseMatrix now keeps track of non zero entries and models show correct number of transitions by referring to nonzero entries rather than all entries in the matrix.  
							
							
 
							
							
							Former-commit-id: 48180be2fe 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c76e0e8d4d 
								
							
								 
							
						 
						
							
							
								
								Added class for initial construct of PRISM programs (to capture position information). Added more validity checks for programs and tests for them (not all though).  
							
							
 
							
							
							Former-commit-id: cf4e985684 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								82836f1ad1 
								
							
								 
							
						 
						
							
							
								
								Added some checks for validity of identifiers in PRISM programs. Added some illegal tests to test suite.  
							
							
 
							
							
							Former-commit-id: fc44db75a7 
							
						 
						12 years ago