David_Korzeniewski
e41922347d
Adapted ExpressionTest.cpp to weird behavior of windows when using temporary shared_ptr in make_pair in initializer_list.
Now using const_pointer_cast instead of static_cast to modify shared pointers. (Although it worked with static_casts, but you never know)
Former-commit-id: d42487bb0c
10 years ago
David_Korzeniewski
07ddaa314c
User declared move constructor and move assignment, as they are currently required to ensure pointer validity.
Former-commit-id: 5e239c60cc
10 years ago
dehnert
f5e383722f
Fixed use of uninitialized value. Deleted assignment operators for classes derived from BaseExpression.
Former-commit-id: 3d6250b393
10 years ago
David_Korzeniewski
8b1a4b4e52
Quickfix s.t. we have a defined index and don't dereference end() which is bad
Former-commit-id: c55bb57dd5
10 years ago
David_Korzeniewski
0f9c753778
Fixed Windows build error
Former-commit-id: a59eafdaf8
10 years ago
dehnert
4f9b5406fe
Fixed simplification of unary expressions.
Former-commit-id: 6644bf5717
10 years ago
dehnert
0a59f7a7ef
Fixed a bug that sometimes prevented transition rewards from being built.
Former-commit-id: afd56375ab
10 years ago
dehnert
40e148d9a4
Added overall performance measurements.
Former-commit-id: bbe4461167
10 years ago
dehnert
8bc646ccb8
Simplification of program when substituting constants.
Former-commit-id: d5ecb355f8
10 years ago
dehnert
072b7d0e1a
Added performance statistics for model building.
Former-commit-id: d7de4f93e3
10 years ago
dehnert
7a55fe9208
Fixed some issues related to conditional probs.
Former-commit-id: c914879d9a
10 years ago
dehnert
5343ea622a
Fixed bug concerning conditional probabilities.
Former-commit-id: be8442deb6
10 years ago
PBerger
e211e269d4
Fix for the Gurobi inclusion.
Former-commit-id: 232a806b4e
10 years ago
PBerger
f7adf54be3
Added A FindGurobi file for CMake.
Adapted build process to use the new file to support all version of the library (upgrading to 6.0 breaks everything).
Former-commit-id: 820ad02968
10 years ago
dehnert
f49d89144e
Fixed issue that could cause wrong models to be generated.
Former-commit-id: 8f1f9b4612
10 years ago
dehnert
2dae5862c8
Small fix to bisimulation options.
Former-commit-id: 555c5ef697
10 years ago
dehnert
ed4f1bb7cf
Added the possibility to build the bisimulation options from a formula in the sense that it automatically picks suitable settings for the formula.
Former-commit-id: 932c7d899a
10 years ago
dehnert
4952306092
Worked on making bisimulation decomposition a bit easier to use.
Former-commit-id: 0fe6b2af6a
10 years ago
dehnert
700703140f
Fixed minor issue.
Former-commit-id: 9799a0cb30
10 years ago
dehnert
9cf82bcd98
Added conversion from transition-based rewards to state-based rewards to enable proper treatment in bisimulation minimization
Former-commit-id: d0c31094bd
10 years ago
dehnert
cc7d44dd15
Added proper canHandle method to propositional model checker.
Former-commit-id: 4af714e31a
10 years ago
dehnert
b5f907d99d
Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation.
Former-commit-id: 517a870d2f
10 years ago
dehnert
18f314d7c6
Some more bugfixes. Damn you, clang on Mac OS!
Former-commit-id: 86a7230a61
10 years ago
dehnert
64fd308713
Another minor bugfix in the formula classes.
Former-commit-id: e1fb3929c7
10 years ago
dehnert
f5b7554590
Minor bugfix for conditional probability computation.
Former-commit-id: c0b103e2aa
10 years ago
dehnert
98efde80f7
Fixed some compile issues (and some other issues).
Former-commit-id: e07861bd92
10 years ago
dehnert
abc222fc31
Fixed some compilation errors.
Former-commit-id: b344bee8d2
10 years ago
David_Korzeniewski
ab36c5fb0d
Workarounds for more Windows quirks. Compiles but tests crash.
Former-commit-id: 0c47ae886d
10 years ago
David_Korzeniewski
7da35af0bb
Some compile errors on Windows fixed, some still persist.
Former-commit-id: 1a9331371b
10 years ago
dehnert
f0a2db6485
Enabled checking formula nodes that contain an expression in the variable of the program.
Former-commit-id: fba632e7f4
10 years ago
dehnert
92aa2607a0
The labels of the models are now only built if no property was given or the given property contains the label.
Former-commit-id: d5ce5a2e1e
10 years ago
dehnert
ee7b591db1
Some work on cli.
Former-commit-id: c3045f48a8
10 years ago
dehnert
c85df2cd74
Conditional Probabilities working. Included two tests.
Former-commit-id: a89255c4ef
10 years ago
dehnert
6bc6753e90
Some work on conditional probs. Not yet working.
Former-commit-id: 1a05e2e5dc
10 years ago
dehnert
ae2b950e86
Fixed some issue in model builder.
Former-commit-id: 12a4afd591
10 years ago
dehnert
9e8d8a2c27
Fixed wrong calculation of reachability rewards in state-elimination-based model checker.
Former-commit-id: bee99d61b0
10 years ago
dehnert
89fc5be1ab
Fixed some things and wrote tests for elimination-based DTMC modelchecker. They fail: apparently rewards are not correctly computed in some cases.
Former-commit-id: 000ad6b049
10 years ago
dehnert
8a4706d9c9
A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
Former-commit-id: bbf988c943
10 years ago
dehnert
b60c5ffdc0
Fixed a lot of tests, improved some things here and there.
Former-commit-id: baec0a4963
10 years ago
dehnert
d0917f033c
Adapted Markov automaton model checker to new formula classes.
Former-commit-id: c351b10ef2
10 years ago
dehnert
89df9621a9
MDP model checker works again.
Former-commit-id: 2c24da6192
10 years ago
dehnert
9026aa9ac9
Adapted first model checker to the new properties.
Former-commit-id: 206d6c9858
10 years ago
dehnert
f673dccd76
Formula parser works again. Tests adapted.
Former-commit-id: 78ce54d69f
10 years ago
dehnert
1699732dce
More work on logic classes.
Former-commit-id: 9d94e02b74
10 years ago
dehnert
4c9d6ccfc5
Removed actions and filters and old logic classes.
Former-commit-id: cd487fd3b3
10 years ago
dehnert
320641e597
Started working on modified property classes.
Former-commit-id: cbcf84c2f6
10 years ago
dehnert
00861a7479
Loosened the restriction to always require GMP a bit.
Former-commit-id: 0537ff217a
10 years ago
dehnert
fafeffe138
Merge branch 'master' into ExpressionModifications
Conflicts:
src/solver/Z3SmtSolver.cpp
Former-commit-id: c195760d33
10 years ago
dehnert
2bd0e2e377
Improved performance of explicit model generation a bit.
Former-commit-id: 1613435eb3
10 years ago
dehnert
91e177028d
Started refactoring explicit model generator of PRISM models
Former-commit-id: 4ea82670d0
10 years ago