Tim Quatmann
|
5dcebdef93
|
Fixed invocation of storm without a model.
|
5 years ago |
|
Tim Quatmann
|
4d55dfbf07
|
Fixed doing non-exact model checking in portfolio engine, even if the --exact switch was set.
|
5 years ago |
|
Tim Quatmann
|
c6b984ca51
|
Do not perform the conversion from a prism program to a jani model twice.
|
5 years ago |
|
Tim Quatmann
|
e3663ee740
|
Portfolio: print true/false instead of 1/0
|
5 years ago |
Matthias Volk
|
ce298fa782
|
Moved signal handling to own file to prevent problems with global static variables being non-unique
|
5 years ago |
|
Matthias Volk
|
f01d8943ad
|
Indicate if result is not fully correct due to abort
|
5 years ago |
|
Tim Quatmann
|
b1dc6fec06
|
Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set.
|
5 years ago |
|
Tim Quatmann
|
ba6f0c0e87
|
BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption.
|
5 years ago |
|
Tim Quatmann
|
c66b0ea442
|
model-handling: Fixed compatibility checks
|
5 years ago |
|
Tim Quatmann
|
54b37d8698
|
Added entry points for portfolio engine
|
5 years ago |
|
Tim Quatmann
|
8711b32c99
|
When using bisimulation with the dd-to-sparse engine, the quotient is automatically extracted in a sparse way.
|
5 years ago |
|
Tim Quatmann
|
1574f4444a
|
CLI: Introduced ModelProcessingInformation which allows to set certain settings (regardinge model building and model verification) in an on-the-fly manner.
|
5 years ago |
|
Tim Quatmann
|
739151af8d
|
CLI: Provide the engine as a parameter in most of the CLI options.
|
5 years ago |
|
Tim Quatmann
|
17325419fb
|
Introduced JIT as a separate engine.
|
5 years ago |
|
Tim Quatmann
|
d36cd93ae8
|
CLI: Split parsing and preprocessing of symbolic input into two steps.
Moved engine related methods and declaration to a separate file.
|
5 years ago |
Sebastian Junges
|
0a6f54f33e
|
a version of parsing choice labels from DRN
|
5 years ago |
|
Sebastian Junges
|
be063dba14
|
POMDPs are now always built with choice labelling and choice indices
|
5 years ago |
Alexander Bork
|
605546358b
|
Added option to merge labels of eliminated states into existing states
|
5 years ago |
|
Alexander Bork
|
e28203fbb8
|
Added option to merge labels of eliminated states into existing states
|
5 years ago |
|
Matthias Volk
|
61c1ec8537
|
Check for Zeno cycles in MA
|
6 years ago |
|
Matthias Volk
|
ddff929cbd
|
Scheduler extraction is only supported for quantitative checks
|
6 years ago |
|
Matthias Volk
|
b0abbb5088
|
Support for k-shortest path counterexamples
|
6 years ago |
|
Matthias Volk
|
bb71c078fa
|
Export to dot format allows for maximal line width in state labels and valuations
|
6 years ago |
|
Matthias Volk
|
9a5a6d72c6
|
Moved some cex code into counterexample module
|
6 years ago |
|
Matthias Volk
|
b8991ca4bf
|
Fixed compile issue due to merge
|
6 years ago |
|
Matthias Volk
|
e4e069a98c
|
Slight refactoring of transformations
|
6 years ago |
|
TimQu
|
9438d56ab3
|
added cli option for transforming continuous time models to discrete time.
|
6 years ago |
|
Tim Quatmann
|
a47945a931
|
Cleaner output when exporting schedulers
|
6 years ago |
|
Tim Quatmann
|
72425ec1b2
|
CLI: Added an option to export the produced scheduler to a file.
|
6 years ago |
|
Alexander Bork
|
450e074c5b
|
Integrated non-Markovian state elimination into Storm MA modelchecking
|
6 years ago |
|
Sebastian Junges
|
d295f6e777
|
export of bdds into dot and text format
|
6 years ago |
|
TimQu
|
eb15177801
|
cli: try to recover after checking a property has failed. (related to GitHub issue #42)
|
6 years ago |
|
Tim Quatmann
|
80bfa6b56e
|
Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set.
|
6 years ago |
|
Matthias Volk
|
87d078f897
|
Output error by STORM_LOG_ERROR
|
6 years ago |
|
TimQu
|
c1119fcd8d
|
Triggered conversion from PRISM to JANI when building an MA with the dd engine since MAs are unsupported in the DdPrismModelBuilder.
|
6 years ago |
|
TimQu
|
19f353591f
|
Added an option to transform CTMCs to MAs and DTMCs to MDPs.
|
6 years ago |
|
TimQu
|
02977da3d7
|
Apply maximum progress assumption while building a Markov Automaton explicitly.
|
6 years ago |
|
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 |
