7e91d5b01e 
								
							
								 
							
						 
						
							
							
								
								Test cases for CSL parser  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								509c1a2b47 
								
							
								 
							
						 
						
							
							
								
								Added support for SteadyStateNoBoundOperator into the CSL parser.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2470c31cb0 
								
							
								 
							
						 
						
							
							
								
								Added SteadyStateNoBoundOperator  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								08815b8c13 
								
							
								 
							
						 
						
							
							
								
								Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement  
							
							
 
							
							
							a "StateNoBoundOperator" now... 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6ff25321d4 
								
							
								 
							
						 
						
							
							
								
								First version of CSL parser  
							
							
 
							
							
							TODO:
- Correct path formulas
- Time bounded until
- Steady state operator without bounds 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9bc8bb2ca8 
								
							
								 
							
						 
						
							
							
								
								Some code style and documentation  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5f9876e4c9 
								
							
								 
							
						 
						
							
							
								
								WIP on CslParser: c6060eb Minor changes (mainly improving comments)  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c3e3ebf1f3 
								
							
								 
							
						 
						
							
							
								
								index on CslParser: c6060eb Minor changes (mainly improving comments)  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c7afcecf4a 
								
							
								 
							
						 
						
							
							
								
								Minor changes (mainly improving comments)  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								da562bcfc9 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into PrctlParser  
							
							
 
							
							
							Conflicts:
	src/modelchecker/AbstractModelChecker.h
	src/modelchecker/GmmxxDtmcPrctlModelChecker.h 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								895c2b6aad 
								
							
								 
							
						 
						
							
							
								
								Convenient file parser for PRCTL, and correct reward formula parsing  
							
							
 
							
							
							(together with some necessary code for that) 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7dc36875ae 
								
							
								 
							
						 
						
							
							
								
								Added file groups in CMakeLists.txt such that files are now grouped in IDEs, like, e.g., Xcode.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d266d9effe 
								
							
								 
							
						 
						
							
							
								
								Fixed another bug in sparse matrix. Fixed bug in test.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2b4d26023a 
								
							
								 
							
						 
						
							
							
								
								Fixed one of the remaining bugs introduced by refactoring.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								00b4797948 
								
							
								 
							
						 
						
							
							
								
								Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9ae177c9b5 
								
							
								 
							
						 
						
							
							
								
								Further refactoring. In particular of the matrix class.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bb441cdeca 
								
							
								 
							
						 
						
							
							
								
								Refactored some parts of sparse matrix.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								840a9b6e07 
								
							
								 
							
						 
						
							
							
								
								Somewhat works now. Still has at least one bug and segfaults afterwards :-)  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e55fca3836 
								
							
								 
							
						 
						
							
							
								
								Implemented module renaming.  
							
							
 
							
							
							This includes clone() routines (that accept the renaming information) for all ir::expressions classes, additional constructors for all ir classes and additional rules in PrismParser.
This is the first version that has the chance to work and actually compiles. (Insert some swearing here...)
Testing is to be done, as this will most probably not work yet. 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								43f11ccc5f 
								
							
								 
							
						 
						
							
							
								
								Refactoring of modelchecker folder.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7ce537adca 
								
							
								 
							
						 
						
							
							
								
								Adding testbed for prismparser  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c1986bcc0e 
								
							
								 
							
						 
						
							
							
								
								Refactored two of the model checker classes.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6c19ddb877 
								
							
								 
							
						 
						
							
							
								
								Cosmetics: Trailing whitespaces, space indentation, ...  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								16c08f7d24 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into PrctlParser  
							
							
 
							
							
							Conflicts:
	examples/mdp/asynchronous_leader/leader3.tra
	examples/mdp/asynchronous_leader/leader4.tra
	examples/mdp/asynchronous_leader/leader5.tra
	examples/mdp/asynchronous_leader/leader6.tra
	examples/mdp/asynchronous_leader/leader7.tra
	examples/mdp/two_dice/two_dice.lab
	examples/mdp/two_dice/two_dice.tra
	src/formula/NoBoundOperator.h
	src/formula/PathBoundOperator.h
	src/formula/ProbabilisticNoBoundOperator.h
	src/formula/RewardNoBoundOperator.h
	src/modelchecker/AbstractModelChecker.h
	src/modelchecker/DtmcPrctlModelChecker.h
	src/modelchecker/EigenDtmcPrctlModelChecker.h
	src/modelchecker/GmmxxDtmcPrctlModelChecker.h
	src/modelchecker/GmmxxMdpPrctlModelChecker.h
	src/modelchecker/MdpPrctlModelChecker.h
	src/models/GraphTransitions.h
	src/parser/AutoParser.h
	src/parser/DeterministicSparseTransitionParser.cpp
	src/parser/NondeterministicModelParser.cpp
	src/parser/NondeterministicSparseTransitionParser.cpp
	src/parser/NondeterministicSparseTransitionParser.h
	src/storage/BitVector.h
	src/storage/SparseMatrix.h
	src/storm.cpp
	src/utility/GraphAnalyzer.h
	src/utility/Vector.h 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0dcebc8ff0 
								
							
								 
							
						 
						
							
							
								
								Start of implementing improved file parser for formulas  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								836bdb3f1c 
								
							
								 
							
						 
						
							
							
								
								Created new base class OptimizingOperator.  
							
							
 
							
							
							Inheriting from this class where appropriate, added constructors accepting minimumOperator argument. 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								78331dfeea 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a5ad38a46b 
								
							
								 
							
						 
						
							
							
								
								Added options for optimizing max/min operator to BoundOperators.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e524720925 
								
							
								 
							
						 
						
							
							
								
								Added prototypical support for in-place matrix-vector multiplication in the style of Gauss-Seidel. This might enhance the speed of convergence for value-iteration model checkers.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								102f38322d 
								
							
								 
							
						 
						
							
							
								
								Fixed several bugs in several modules (bit vector, parser, etc.). Topological value iteration now works for the consensus protocol and the two dice example.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								49ac740459 
								
							
								 
							
						 
						
							
							
								
								Changed a bit, how log messages are processed.  
							
							
 
							
							
							Thresholds are now as follows:
main logger INFO, consoleAppender WARN, fileAppender none (i.e. everything)
--verbose changes consoleAppender to INFO
--debug changes main logger and consoleAppender to DEBUG 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								525fc7c16f 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c784de4d03 
								
							
								 
							
						 
						
							
							
								
								Added new model checker that uses topological value iteration. However, does not fully work yet.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bb6afcb1fd 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1f3b172c83 
								
							
								 
							
						 
						
							
							
								
								Added a simple module that handles segfaults: print a message and provide a backtrace.  
							
							
 
							
							
							I grew tired of always starting gdb when it would've sufficed to know the function.
This routine will demangle C++ symbols, so you can see in which function we crashed. 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								17e0e8165a 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bdf173c315 
								
							
								 
							
						 
						
							
							
								
								GraphTransition objects can now be build from the SCC decomposition of a system.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e4129c37d9 
								
							
								 
							
						 
						
							
							
								
								fixed two bugs in ExplicitModelAdapter.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5c25116a24 
								
							
								 
							
						 
						
							
							
								
								First version of ExplicitModelAdapter that supports transition rewards.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d9e833680a 
								
							
								 
							
						 
						
							
							
								
								Added convenience methods RewardModel::hasStateRewards() and RewardModel::hasTransitionRewards()  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7dc5324a65 
								
							
								 
							
						 
						
							
							
								
								Program returns empty RewardModel and emits error, if invalid model is given.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								928de19fed 
								
							
								 
							
						 
						
							
							
								
								Reorganized main routine. Catching errors that made it to the top level.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								341dc50ab7 
								
							
								 
							
						 
						
							
							
								
								Added some better error output for basic parsers using errno  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8dce5af515 
								
							
								 
							
						 
						
							
							
								
								fixed some warnings (comparison between signed/unsigned)  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								75ce91082a 
								
							
								 
							
						 
						
							
							
								
								Forgot to commit actual cpp file...  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a73ae7aed4 
								
							
								 
							
						 
						
							
							
								
								Added new option --debug.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2bc32fe3de 
								
							
								 
							
						 
						
							
							
								
								Cleaned up handling of --verbose, proposing correct use of log levels from now on...  
							
							
 
							
							
							FATAL_LOG_LEVEL: Use, if we are going to crash.
ERROR_LOG_LEVEL: Use, if there is no reasonable way to continue.
WARN_LOG_LEVEL: Use, if we got something the average user should read.
INFO_LOG_LEVEL: Use, if this might in some cases be of interest.
DEBUG_LOG_LEVEL: Use, if this should usually not be relevant to a user.
TRACE_LOG_LEVEL: Use only during development.
There are three levels of verbosity:
- default: WARN and above
- verbose: INFO and above
- debug: DEBUG and above 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5f64fd168b 
								
							
								 
							
						 
						
							
							
								
								Cleaned up structure of ExplicitModelAdapter.  
							
							
 
							
							
							- added cpp file
- returns complete models now (missing transition rewards...) 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f52d4eb7a8 
								
							
								 
							
						 
						
							
							
								
								Added new option --debug.  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								fd30e8ca25 
								
							
								 
							
						 
						
							
							
								
								Cleaned up handling of --verbose, proposing correct use of log levels from now on...  
							
							
 
							
							
							FATAL_LOG_LEVEL: Use, if we are going to crash.
ERROR_LOG_LEVEL: Use, if there is no reasonable way to continue.
WARN_LOG_LEVEL: Use, if we got something the average user should read.
INFO_LOG_LEVEL: Use, if this might in some cases be of interest.
DEBUG_LOG_LEVEL: Use, if this should usually not be relevant to a user.
TRACE_LOG_LEVEL: Use only during development.
There are three levels of verbosity:
- default: WARN and above
- verbose: INFO and above
- debug: DEBUG and above 
							
						 
						13 years ago