dehnert
|
5beb33e3d8
|
merged a bit more
Former-commit-id: e42dc21233
|
11 years ago |
dehnert
|
61fb277024
|
more work on refactoring (storm stinks and should be rewritten :P)
Former-commit-id: 7495dea2df
|
11 years ago |
sjunges
|
92082dc970
|
gurobi lp solver refactored in case gurobi is not found, and fixes for linux - sorry about earlier lack of checks on linux
Former-commit-id: badef77583
|
11 years ago |
sjunges
|
f85d28325e
|
Further work towards faster and more modular compilation
Former-commit-id: 9de50910b8
|
11 years ago |
sjunges
|
3c2040f4b7
|
Removed many superfluous includes, added some source files -- towards faster compilation
Former-commit-id: a575a97d40
|
11 years ago |
dehnert
|
b56766e993
|
more work on reward model that turned out to be refactoring in disguise
Former-commit-id: 31a7fa4801
|
11 years ago |
sjunges
|
a129983ae9
|
cleaning includes for better compilation times
Former-commit-id: e2878ae043
|
11 years ago |
dehnert
|
6fa1078fb1
|
some more work on reward model
Former-commit-id: 8533357f34
|
11 years ago |
dehnert
|
dcd42d5653
|
started reworking reward models
Former-commit-id: 49d9106451
|
11 years ago |
sjunges
|
812b101c40
|
better program checks, some extensions in model and matrix
Former-commit-id: 8efaaf2ca9
|
11 years ago |
sjunges
|
2e0c9c1244
|
unification of some constructs in carl propagated to storm
Former-commit-id: 34ba08debf
|
11 years ago |
dehnert
|
f879c608eb
|
fix for wrong ifdef
Former-commit-id: dd17e10d08
|
11 years ago |
dehnert
|
ecb37ccd1d
|
made compilation of ConstraintCollector in Dtmc predicated on CARL being available
Former-commit-id: 8d0e3ea636
|
11 years ago |
sjunges
|
7a050434d9
|
bugfixes for NondeterministicModel, improvements for StateActionPair, graph and initialize
Former-commit-id: 4531d784a1
|
11 years ago |
sjunges
|
a212cce8c1
|
Added a method to get the number of choices for a specific state.
Former-commit-id: 1ced589a95
|
11 years ago |
dehnert
|
9d5c3e7e2f
|
added functionality to flatten the modules of a PRISM program into one module
Former-commit-id: 04faac9c67
|
11 years ago |
dehnert
|
4dbbe3c561
|
moved constraint collection to DTMC class
Former-commit-id: 5471a20bec
|
11 years ago |
dehnert
|
81c627b9b7
|
First version of fully symbolic game solver.
Former-commit-id: 34406f25b9
|
11 years ago |
dehnert
|
96464fdcbc
|
added model classes for two-player stochastic games
Former-commit-id: 8dccae2ea9
|
11 years ago |
dehnert
|
37cd2ad682
|
started working on game solver
Former-commit-id: 59c3528d23
|
11 years ago |
dehnert
|
76b99a5515
|
Commit to switch workplace.
Former-commit-id: e80da5e90b
|
11 years ago |
dehnert
|
3b4dca1a03
|
Improved Jacobi method a bit.
Former-commit-id: f4affeebf6
|
11 years ago |
dehnert
|
06bfc17ec6
|
Started making hybrid (dd/sparse) model checking work.
Former-commit-id: 23fac3a672
|
11 years ago |
dehnert
|
d787b80fec
|
CTMC examples now build properly using the DD-based model generator.
Former-commit-id: ac97b005e3
|
11 years ago |
dehnert
|
9d66f5128e
|
Further work on symbolic CTMC generation.
Former-commit-id: 81f2efb98c
|
11 years ago |
dehnert
|
60701cebdb
|
ADDs and BDDs are no longer mixed in the abstraction layer.
Former-commit-id: 3c31063ea6
|
11 years ago |
dehnert
|
a851fad65d
|
More work on reward properties for CTMCs.
Former-commit-id: 860fee54c7
|
11 years ago |
dehnert
|
65bf06dd50
|
Further steps towards CTMC model checking.
Former-commit-id: f057eeb17e
|
11 years ago |
dehnert
|
00e7121bc4
|
some work towards BDD-based mc.
Former-commit-id: cae0c4421e
|
11 years ago |
dehnert
|
c70d93f4d3
|
Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.
Former-commit-id: 3215a38c44
|
11 years ago |
dehnert
|
1a1906f811
|
Added functional tests for DD-based and sparse computation of states with prob 0 and 1.
Former-commit-id: a62c67c657
|
11 years ago |
dehnert
|
c8007876ae
|
Symbolic models can now be built from the command line.
Former-commit-id: 2c239df754
|
11 years ago |
dehnert
|
239caf57eb
|
Added symbolic models and made DD-based model generator build the correct instances.
Former-commit-id: c054401cfd
|
11 years ago |
dehnert
|
f0b174b756
|
Fixed performance tests.
Former-commit-id: f58e2eb923
|
11 years ago |
dehnert
|
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 |
David_Korzeniewski
|
b623384dda
|
Fixed merge errors and adapted to changes in master
Former-commit-id: 08054e7bec
|
11 years ago |
dehnert
|
c3c83fbe4f
|
Fixed some compilation errors.
Former-commit-id: dc626450b8
|
11 years ago |
dehnert
|
4952306092
|
Worked on making bisimulation decomposition a bit easier to use.
Former-commit-id: 0fe6b2af6a
|
11 years ago |
dehnert
|
700703140f
|
Fixed minor issue.
Former-commit-id: 9799a0cb30
|
11 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
|
11 years ago |
David_Korzeniewski
|
ee4c961cc9
|
fixes for compile errors. target "storm" builds without errors
tests not compiling because of property modifications.
Former-commit-id: 0366cf99cd
|
11 years ago |
David_Korzeniewski
|
3e4495cad0
|
small fixes
Former-commit-id: 0d9cc58d75
|
11 years ago |
dehnert
|
01bd1fbc76
|
Model building works again for parametric systems.
Former-commit-id: d3f3e357ca
|
11 years ago |
dehnert
|
2bd0e2e377
|
Improved performance of explicit model generation a bit.
Former-commit-id: 1613435eb3
|
11 years ago |
dehnert
|
5e37c09fc0
|
Fixed some bugs.
Former-commit-id: dce463081d
|
11 years ago |
dehnert
|
91084a5da4
|
APs true/false can now be queried for a state.
Former-commit-id: 3c16df4509
|
11 years ago |
dehnert
|
5676d990c4
|
APs true/false can now be queried for a state.
Former-commit-id: 0157e03340
|
11 years ago |
dehnert
|
843a1d1fdf
|
Added comparator use for checking validity of probability matrices such that only if the value is actually constant it is required to be one.
Former-commit-id: 3224422976
|
11 years ago |
dehnert
|
aa6e44a1e2
|
Some fixes after merge.
Former-commit-id: 5df69ca655
|
11 years ago |
dehnert
|
1c091d7640
|
Renamed some classes to indicate that only strong bisimulation can be computed. Added option to start with an initial partition that preserves only certain formulas. Added ConstantsComparator concept that is to be used when constants have to be compared with other constants.
Former-commit-id: feacadfa38
|
11 years ago |