Tim Quatmann
|
44be19f274
|
Added missing treatment of SMGs in API method.
|
5 years ago |
|
Tim Quatmann
|
efce929c5f
|
Potentially allow verification of SMGs over RationalNumbers
|
5 years ago |
 Stefan Pranger
|
6701c61178
|
verification now handles SMGs
|
5 years ago |
|
Tim Quatmann
|
211a72b6d7
|
fixing compilation of storm-pars
|
5 years ago |
|
Tim Quatmann
|
2e593dc014
|
Added computation of steady state probabilities for DTMC/CTMC in the sparse engine.
|
5 years ago |
|
Tim Quatmann
|
28ab011eb8
|
Added an export of check results to json.
|
5 years ago |
|
TimQu
|
b45497a8c4
|
Added --propsasmulti switch to interpret input formulas as multi-objective formula
|
6 years ago |
Sebastian Junges
|
923f779a09
|
explicit-state-lookup, for finding states in a model based on the variable assignment
|
6 years ago |
|
Sebastian Junges
|
d6bfcb4818
|
refactoring: moving some code out of the util folder
|
6 years ago |
|
Tim Quatmann
|
073d2affa4
|
api/verification: Added a missing include
|
6 years ago |
|
Sebastian Junges
|
1a6f2e6fba
|
--io:nodrnplaceholders
|
6 years ago |
|
Tim Quatmann
|
feebf1a24d
|
Added scheduler export in .json
|
6 years ago |
|
Tim Quatmann
|
5d530bb532
|
Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards)
|
6 years ago |
|
Tim Quatmann
|
04c2938057
|
Introduced hybrid engine for Markov automata (only reach. rewards for now)
|
6 years ago |
|
Tim Quatmann
|
f7e2ff0843
|
Apply max. Prog. assumption while building with the dd engine.
|
6 years ago |
|
Tim Quatmann
|
ba6f0c0e87
|
BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption.
|
6 years ago |
|
Tim Quatmann
|
a99f0905e2
|
dd/bisimulation: Added argument to "getQuotient" which allows to set the quotient type (dd / sparse)
|
6 years ago |
|
Tim Quatmann
|
ac35a04eec
|
utility/engine: canHandle(...) compiles now.
Moved getSupportedJaniFeatures to builder/BuilderType.
|
6 years ago |
Sebastian Junges
|
0a6f54f33e
|
a version of parsing choice labels from DRN
|
6 years ago |
|
Sebastian Junges
|
be3ff1520f
|
export in api can be called without explicitly giving parameter names
|
6 years ago |
Alexander Bork
|
605546358b
|
Added option to merge labels of eliminated states into existing states
|
7 years ago |
|
Alexander Bork
|
e28203fbb8
|
Added option to merge labels of eliminated states into existing states
|
7 years ago |
Matthias Volk
|
bb71c078fa
|
Export to dot format allows for maximal line width in state labels and valuations
|
7 years ago |
|
Matthias Volk
|
e4e069a98c
|
Slight refactoring of transformations
|
7 years ago |
|
TimQu
|
9438d56ab3
|
added cli option for transforming continuous time models to discrete time.
|
7 years ago |
|
Matthias Volk
|
628219298e
|
Some small cleanup in verification API
|
7 years ago |
|
Tim Quatmann
|
429c91ff13
|
Added support for parsing fractions in DRN files.
|
7 years ago |
|
Tim Quatmann
|
72425ec1b2
|
CLI: Added an option to export the produced scheduler to a file.
|
7 years ago |
|
Alexander Bork
|
450e074c5b
|
Integrated non-Markovian state elimination into Storm MA modelchecking
|
7 years ago |
|
Sebastian Junges
|
d295f6e777
|
export of bdds into dot and text format
|
7 years ago |
|
Matthias Volk
|
267efd692a
|
Construct time reward model
|
7 years ago |
|
Matthias Volk
|
dfd1fec8c5
|
Fixed compile issues
|
7 years ago |
|
TimQu
|
66ab97ba4f
|
transformer: Added functionality to also translate expected time formulas to expected rewards.
|
7 years ago |
|
TimQu
|
19f353591f
|
Added an option to transform CTMCs to MAs and DTMCs to MDPs.
|
8 years ago |
|
TimQu
|
8a7a604f4c
|
Fixed actually taking options for non-deterministic bisimulation when performing non-deterministic bisimulation.
|
8 years ago |
|
Sebastian Junges
|
f2850f9e6f
|
verification api now takes (optionally) the environment as a first parameter, to make code less dependent on global setttings objects
|
8 years ago |
|
TimQu
|
37eb90bc82
|
better check whether transition rewards can be scaled and lifted to action rewards
|
8 years ago |
|
TimQu
|
2dd5c65051
|
fixed duplicated symbol linker error
|
8 years ago |
|
TimQu
|
101b49b898
|
detect unsupported jani-features directly upon parsing the model.
|
8 years ago |
dehnert
|
c3d40d634b
|
started working on the github issues by Linda
|
8 years ago |
|
dehnert
|
51be532695
|
pulled out parsing from abstraction-refinement classes
|
8 years ago |
|
TimQu
|
d9ec0f8fcf
|
removed include of old janiexportsettings
|
8 years ago |
|
TimQu
|
86f0195b18
|
removed jani conversion in cli of main binary
|
8 years ago |
|
Sebastian Junges
|
54c0bbb7c3
|
flatten of jani models before export via appropriate setting
|
8 years ago |
|
Sebastian Junges
|
e64e293d59
|
jani transformer which changes a variable into a location
|
8 years ago |
|
dehnert
|
9d528db2fc
|
adding translation of expressions used in formulas to symbolic-to-sparse transformers
|
8 years ago |
|
Sebastian Junges
|
98969e627c
|
updated counterexamples to support statistics to be exported
|
8 years ago |
|
sjunges
|
79bb6734ed
|
compile and link parsers in seperate binary
|
8 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
|
8 years ago |
Joachim Klein
|
b6d67e7995
|
properties.cpp: Output warning if we filter away all properties
|
8 years ago |
