TimQu
|
240faff125
|
BuilderOptions: Added terminal states for bounded until and reachability reward formulas.
|
7 years ago |
|
TimQu
|
605c13238e
|
Correctly handle the case where no model description is provided to the builder options.
|
7 years ago |
|
TimQu
|
02977da3d7
|
Apply maximum progress assumption while building a Markov Automaton explicitly.
|
7 years ago |
|
TimQu
|
b3987b178c
|
Explicit model builder: Give an error if no initial state is found.
|
7 years ago |
|
TimQu
|
37eb90bc82
|
better check whether transition rewards can be scaled and lifted to action rewards
|
7 years ago |
dehnert
|
acfb8d28c0
|
fixing issues related to rewards in JIT-based model builder
|
7 years ago |
|
dehnert
|
e745ddbe0d
|
some fixes related to DD-based JANI model building
|
7 years ago |
|
dehnert
|
54a7c84725
|
started fixing some issues related to transient variable assignments in DD-based JANI model builder
|
7 years ago |
|
dehnert
|
3811c3f0b4
|
converting error on missing action in JANI DD-builder to warning
|
7 years ago |
Matthias Volk
|
eb6fa09ef8
|
Fixed warning for initialization order
|
7 years ago |
|
TimQu
|
6e37bd3271
|
fixed an issue with building MAs via jit
|
7 years ago |
|
TimQu
|
02fdc292fd
|
handling non-trivial reward expressions in jani-builders
|
7 years ago |
|
TimQu
|
5ab404a9d3
|
added support for unbounded integer variables in explicit jani builder such that it is treated as a bounded variable (with a given number of bits) and an exception is thrown in case of an underflow or overflow
|
7 years ago |
|
TimQu
|
c95ca4ed15
|
All model builders support state-exit rewards
|
7 years ago |
|
TimQu
|
71489a24f5
|
The model builders now substitute jani functions (if still present)
|
7 years ago |
|
TimQu
|
101b49b898
|
detect unsupported jani-features directly upon parsing the model.
|
7 years ago |
|
TimQu
|
7c61a16d91
|
fixes for array expressions, support to translate properties that consider array expressions, translating array models in cli
|
7 years ago |
|
TimQu
|
6aaafea554
|
added possibility to lift transient edge destination assignments to the edge by scaling with the probability (only if this preserves the considered properties).
|
7 years ago |
|
TimQu
|
e2cb68b31f
|
Enable array elimination in jit builder
|
7 years ago |
|
TimQu
|
4302aa0be0
|
added missing include
|
7 years ago |
|
dehnert
|
264d9158c8
|
bugfix for dd-based MA building from JANI
|
7 years ago |
|
Matthias Volk
|
6b91485382
|
Removed redundant file
|
7 years ago |
Sebastian Junges
|
f52aab0012
|
fixed out-of-bounds-labelling, added overlapping guards building, and some improved error messages if something goes wrong with highlevel counterex generation
|
7 years ago |
|
Sebastian Junges
|
91bbe85a07
|
builder options for labeling overlapping guards
|
7 years ago |
|
Sebastian Junges
|
61925d1c98
|
add option for sparse model builder to add a state encoding out-of-bounds state valuations to enable analysis of buggy models
|
7 years ago |
|
Matthias Volk
|
2658a02604
|
Fixed compiler warnings for unused lambda captures
|
7 years ago |
|
dehnert
|
1169195be7
|
some fixes (in particular for warnings)
|
7 years ago |
|
dehnert
|
316412c5d3
|
fixed a bug related to closing symbolic Markov automata
|
8 years ago |
|
dehnert
|
8482063a16
|
made symbolic bisimulation work with MA and support of sparse quotient extraction for MA
|
8 years ago |
|
dehnert
|
9e5e1980dd
|
first working version of symbolic Markov automaton bisimulation
|
8 years ago |
|
dehnert
|
017d4abd84
|
first steps towards symbolic MA building
|
8 years ago |
|
dehnert
|
24d6337006
|
JANI choice origins and MILP-based high-level cex for JANI
|
8 years ago |
|
dehnert
|
d45eead440
|
improved asserted constraints for high-level cex
|
8 years ago |
|
dehnert
|
59666a9fe9
|
slight renaming in matrix builder to better capture semantics
|
8 years ago |
|
dehnert
|
99647c11fb
|
fixed an issue pointed out by Tim
|
8 years ago |
|
dehnert
|
1f9e2967c8
|
some optimizations in explicit model building
|
8 years ago |
|
dehnert
|
ac759d2671
|
minor performance improvements to model building
|
8 years ago |
|
dehnert
|
6501fffac3
|
several optimizations related to explicit model building
|
8 years ago |
sjunges
|
12dda40919
|
split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs
|
8 years ago |
|
dehnert
|
3a11914da0
|
commit to switch workplace
|
8 years ago |
|
Matthias Volk
|
20a76f01e2
|
Better error output for jit
|
8 years ago |
|
dehnert
|
2d41de479e
|
added progress outputs to iterative solvers
|
8 years ago |
|
dehnert
|
0c5aa1645d
|
fix reward model generation in JIT builder
|
8 years ago |
|
sjunges
|
3ac42caf7c
|
extensions to pomdp stuff
|
8 years ago |
|
sjunges
|
9314d99354
|
allow inference from actions, but only with a set option
|
8 years ago |
|
dehnert
|
11d2ee2fda
|
making sure to add meta variables to transition matrix DD to make sure one can abstract from them later
|
8 years ago |
|
dehnert
|
36554b5b87
|
fixed some issues with reward preservation in dd-based bisimulation
|
8 years ago |
|
dehnert
|
9a6abf7eec
|
fixed a bug in dd-based reward model building
|
8 years ago |
|
Sebastian Junges
|
09dcb149c2
|
storm parses and builds pomdps
|
8 years ago |
|
sjunges
|
bbb4d16965
|
towards support for pomdps in storm
|
8 years ago |
