* Created a distinct parser for each expression type and for identifiers
* Removed all expression rules from PrismParser, using new parsers instead
* Reduced excessive usage of boost::lambda, using semantic actions only for single calls
* Moved actual state to new class (-> VariableState, whole two-run-logic can probably implemented there)
* Much cleanup
Work should be finished on expression parser, but not yet on prism parser...
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.
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
* Removed templates from various functions, as we can only produce double models anyway.
* Added methods to compute state rewards and state labelings
* Added toModel() routine
The new adapter will generate an intermediate datastructure that holds all transitions to be inserted.
This will combine the two phases (computing the state space and actually generating the matrix) and can also be used for dtmc and mdp models.
This datastructure is only a list of maps for each state. Each map represents a nondeterministic choice and maps target node ids to their probability.
Added new helper routines:
* getActiveCommandsByAction() retrieves commands that are active (i.e. guard is true) for some action.
* applyUpdate() copies a given state and updates it with a given update.
Added state expansion for synchronized commands.
Made former loop only consider unsynchronized commands.
gereon
dehnert