c8e8e1502b
Added minimum/maximum support for probablistic no bound operators.
12 years ago
f9ab6f85d0
- Restructuration of model checkers (by logic)
- LTL file parser
12 years ago
aafdbf7671
Fixed errors due to merging.
12 years ago
5495456991
Added new log level "trace"
Fixed bug in ExplicitModelAdapter
12 years ago
065ac8f659
Basic command line interface for SToRM
12 years ago
5d3b9e5cc1
Basic structure for central model checking method in storm.cpp
12 years ago
3b5602b942
Reduction of functionality of fileParser: Only does the parsing, no
checking
12 years ago
cc242974dc
Renamed namespace storm::formula to storm::property
12 years ago
dfd4df2884
Removing debug output.
12 years ago
a790a7c3ec
Allow != as a token.
12 years ago
6ad0c7041e
Allow DoubleExpressions to use integer constants
12 years ago
ac86932785
Fixed renaming: Command names were not considered.
12 years ago
3b76126f6b
Split PrismParser and PrismGrammar in differenc object files.
Added reset method for grammars, now we can parse multiple files in one program execution.
Added test for mdp parsing.
12 years ago
4222130524
Fixed a few more bugs in clone() of various Expression classes and some in the module renaming.
12 years ago
5840ca5bab
Fixed weird error from previous commit.
12 years ago
c3cfc5404c
Somewhat fixed weird issue during module renaming.
The "fix" is very weird (see VariableState.cpp:55 and following) and still seems to lead to a segfault upon program termination...
12 years ago
f09be5c3b4
Made BaseGrammar constructor clang-compatible, fixed ms output of CPU usage
12 years ago
ac313cb997
Removed debug output, fixed DoubleExpressionGrammar
12 years ago
014ecd8597
Fixed some glitches, producing meaningful error if sum of probabilities for a command is not one
12 years ago
c1801b4ecc
Changed debug output to use LOG4CPLUS
12 years ago
a9edf2aa8c
Removed some debug output.
12 years ago
9613d099bb
Removed shared_ptr for module, program and rewardmodel objects.
12 years ago
1878962dea
Fixed another nullptr, removed shared_ptr for Update and Command objects.
12 years ago
d0adf9d1b3
Some more test cases and, resulting from those, minor changes in LTL
parser.
12 years ago
01b1efc12d
Some improvements/corrections to the LTL parser and some test cases for
it
12 years ago
834cb269a6
Minor corrections in code
12 years ago
3c1cf4819c
Fixed a few other issues. Module renaming seems to work now!
(However, there is still a segfault at some later point...)
12 years ago
152bcd2f20
Porting Program datastructures to use shared_ptr (at least for the moment...)
some more cleanups
12 years ago
b92260fed0
A lot of work on PrismParser:
* 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...
12 years ago
00286b2f01
Added formula classes for CSL
12 years ago
f513e49084
Almost finished restruction of PRCTL formulas; adapted code (including
test cases) to work correctly with the new structure
12 years ago
bb37bc49f2
Compiling version of PrismParser.
13 years ago
39ff3240d3
More convenient syntax for time bounded formulas, and respective test
cases.
13 years ago
35baa5ff02
Added parsing of time bounded operators
13 years ago
7e91d5b01e
Test cases for CSL parser
13 years ago
509c1a2b47
Added support for SteadyStateNoBoundOperator into the CSL parser.
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
c7afcecf4a
Minor changes (mainly improving comments)
13 years ago
895c2b6aad
Convenient file parser for PRCTL, and correct reward formula parsing
(together with some necessary code for that)
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
6c19ddb877
Cosmetics: Trailing whitespaces, space indentation, ...
13 years ago
0dcebc8ff0
Start of implementing improved file parser for formulas
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
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
752dda4252
fixing error with difference operator in freeIdentifier
13 years ago
c7f58ed5f5
Modified parsers such that the reward matrices are of the same size as the transition matrices.
13 years ago
Lanchid
gereon
dehnert