TimQu
|
c27b8af90f
|
Display the time required for parsing the prism/jani input
|
7 years ago |
|
TimQu
|
0434d9f83a
|
fixed issue when checking whether transition rewards can be lifted
|
7 years ago |
dehnert
|
e745ddbe0d
|
some fixes related to DD-based JANI model building
|
7 years ago |
|
TimQu
|
bf40fb54f2
|
added api call that directly applies a given jani-property filter
|
7 years ago |
|
TimQu
|
019cc8b1a0
|
preserved order of jani-properties as given in the file
|
7 years ago |
|
TimQu
|
31a67afa4a
|
also print filtered rationalNumber checkresults as double
|
7 years ago |
|
TimQu
|
ee9e6354a3
|
removed standard-compliant option: storm-conv now produces standard compliant jani code by default
|
7 years ago |
|
TimQu
|
55efedb713
|
prism2jani no longer fails if a reward model has the same name as a formula/variable
|
7 years ago |
|
TimQu
|
101b49b898
|
detect unsupported jani-features directly upon parsing the model.
|
7 years ago |
|
TimQu
|
c739f0befa
|
elimination of jani function
|
7 years ago |
|
TimQu
|
2febe36a65
|
removed dependency on storm-conv
|
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 |
|
dehnert
|
6ab7859c84
|
fixing more of Lindas issues
|
7 years ago |
|
dehnert
|
51be532695
|
pulled out parsing from abstraction-refinement classes
|
7 years ago |
|
TimQu
|
8050f8fc67
|
eliminate reward accumulations on jani level
|
7 years ago |
|
TimQu
|
831f07e867
|
eliminate reward accumulations whenever possible
|
7 years ago |
|
TimQu
|
910b6e6b22
|
fixed wrong include
|
7 years ago |
|
TimQu
|
0fa361c393
|
displaying property name together with the property
|
7 years ago |
|
TimQu
|
35aa166f5b
|
added possibility to check all available jani properties
|
7 years ago |
|
TimQu
|
86f0195b18
|
removed jani conversion in cli of main binary
|
7 years ago |
|
dehnert
|
9d528db2fc
|
adding translation of expressions used in formulas to symbolic-to-sparse transformers
|
7 years ago |
|
TimQu
|
0c0f61e27b
|
Fix: Only access counterexample settings in model-handling, if they are available.
|
7 years ago |
Sebastian Junges
|
0be0126095
|
fixed support for highlevel counterex for expected rewards in dtmcs
|
7 years ago |
sjunges
|
79bb6734ed
|
compile and link parsers in seperate binary
|
7 years ago |
|
sjunges
|
6dfce6a405
|
extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times
|
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 |
|
dehnert
|
21c970f8f7
|
added dd-to-sparse engine that builds the model as a DD and then transforms the whole model to a sparse representation
|
7 years ago |
|
dehnert
|
09866e4577
|
enabling changing value type in quotient extraction of dd-bisimulation
|
7 years ago |
|
dehnert
|
5f7cd17789
|
added printing info when value type is converted after preprocessing
|
7 years ago |
|
dehnert
|
139752eb66
|
added option to perform dd-bisimulation using exact arithmetic
|
7 years ago |
|
dehnert
|
9e5e1980dd
|
first working version of symbolic Markov automaton bisimulation
|
7 years ago |
|
dehnert
|
4d7be96dda
|
MaxSAT-based high-level counterexamples for JANI
|
7 years ago |
|
dehnert
|
24d6337006
|
JANI choice origins and MILP-based high-level cex for JANI
|
7 years ago |
|
dehnert
|
4591dba631
|
made maxsat-based counterexample generation be applicable to DTMCs and MDPs
|
7 years ago |
|
dehnert
|
0d18886966
|
re-enabling conversion of MA to CTMC if the MA only has Markovian states
|
7 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
|
c85e30dfd0
|
added distance-aware initial partition to dd-based bisimulation
|
8 years ago |
|
dehnert
|
b415c12c25
|
further preparation of partial bisimulation model checker
|
8 years ago |
|
dehnert
|
9c685f3bdb
|
started on partial bisimulation model checker
|
8 years ago |
|
dehnert
|
bf727a28fd
|
remove debug output and choose sylvan automatically in exact mode
|
8 years ago |
Matthias Volk
|
e5387ecc85
|
Deactivated conversion to CTMC for trivial non-determinism in MA as it is not correct at the moment
|
8 years ago |
|
dehnert
|
e557a8e069
|
started on EC elimination for hybrid engine
|
8 years ago |
|
dehnert
|
2d41de479e
|
added progress outputs to iterative solvers
|
8 years ago |
|
TimQu
|
fcd277c42a
|
added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format
|
8 years ago |
|
dehnert
|
68f14c728a
|
added missing check for existence of model
|
8 years ago |
|
dehnert
|
b4bfd0c39f
|
performance improvement in DS-MPI; some cleanups
|
8 years ago |
|
dehnert
|
df0b5fbfa5
|
fixed multiply-reduce operations in the presence of empty row groups
|
8 years ago |
|
Sebastian Junges
|
e0452be54b
|
move some of the cli stuff to an own header
|
8 years ago |
|
sjunges
|
e718acffba
|
move cli stuff from storm lib to an own small lib
|
8 years ago |
|
sjunges
|
2c2dc5acd8
|
Changed API such that the command line settings do not occur in the settings anymore. Moreover, to prevent having 15 Boolean arguments, the build options are now part of the API.
|
8 years ago |
