TimQu
b3edae8707
fixed fragment specification: total reward formulas should not be supported for hybrid/dd right now
7 years ago
Alexander Bork
8c3bd15eae
Fixed priorities for dependencies and export of PDEP probabilities into PNPRO format
7 years ago
Matthias Volk
7dc17065c1
Updated DFT export to new JSON format
7 years ago
Sebastian Junges
0be0126095
fixed support for highlevel counterex for expected rewards in dtmcs
7 years ago
Sebastian Junges
73a1911a53
Merge branch 'master' into counterexample_improvements
7 years ago
Alexander Bork
1850cf7368
Fixed trigger rates for timed transitions not being saved in .pnpro files
7 years ago
TimQu
c2dd57cda5
total rewards for mdps
7 years ago
TimQu
87e34d7b32
Added Support for Total Reward Formulas for DTMCs in the Sparse Engine
7 years ago
TimQu
e4817759df
policy iteration based weight vector checker
7 years ago
TimQu
aece3020f6
improved functionality of the scheduler evaluator
7 years ago
dehnert
dfc0141894
minor fix to Z3 API modification
7 years ago
dehnert
cdfa328464
first attempt at adapting to Z3 interface change
7 years ago
TimQu
bf973187c4
use deterministicParetoExplorer in case there is a scheduler restriction.
7 years ago
TimQu
a638104adb
using new post processing class for the 'old' implementation.
7 years ago
TimQu
80a66603fb
added possibility to compute the 'downward closure' of a polytope only with respect to a set of dimensions
7 years ago
TimQu
136084af75
started implementing deterministic scheduler finding approach for multi-objective model checking
7 years ago
Matthias Volk
1f221db280
Disable transformation of DFT properties to JANI
7 years ago
Matthias Volk
eea940b625
Refactoring for transformation DFT->GSPN->JANI
7 years ago
dehnert
4134630fa6
adding gap output
7 years ago
Alexander Bork
758382e020
Merge remote-tracking branch 'origin/dft_gspn' into dft_gspn
7 years ago
Alexander Bork
a49f88b7f5
Fixed computation of priorities to correctly represent the semantics
7 years ago
dehnert
4f4d1f4423
do not scale precision
7 years ago
Matthias Volk
a6e6d5993f
Travis: set unlimited clone depth to allow versioning with git describe
7 years ago
Matthias Volk
0d4cf67f2e
Set mergeDC from setting
7 years ago
Matthias Volk
cf316df35e
Added settings for DFT-GSPN transformation
7 years ago
Matthias Volk
afb0be1245
Fixed missing dependencies to storm-parsers
7 years ago
Matthias Volk
9e398ffaab
Minor improvements for some CMake output
7 years ago
dehnert
386f0b2e47
fixing bug in scheduler improvement step of policy iteration for games
7 years ago
Matthias Volk
369cea775d
Swapped order in PriorityQueue to propagate failures in correct order
7 years ago
sjunges
8478352030
dynamic constraints and minimality labels
7 years ago
dehnert
2aff2e9382
adding some more timing output
7 years ago
sjunges
53238f43f7
fixed some missing includes due to updated API
7 years ago
sjunges
39698d6ecb
fix install of storm-counterexamples
7 years ago
sjunges
79bb6734ed
compile and link parsers in seperate binary
7 years ago
sjunges
3a704ae532
fix storm-dft missing includes
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
dehnert
b0047a5a96
improving choices in game policy iteration depending on precision of underlying solver
7 years ago
sjunges
6fcc91b9d0
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
7 years ago
Sebastian Junges
d1ab260068
remove outdated parts in highlevel counterexamplse
7 years ago
Sebastian Junges
e29e6c7cd2
high level counterexamples extended with more options, and improved performance when minimizing over a subset
7 years ago
sjunges
ade4b5bf72
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
7 years ago
dehnert
48f5608157
making policy iteration available for game-based abstraction (prototypical for now)
7 years ago
Joachim Klein
b6d67e7995
properties.cpp: Output warning if we filter away all properties
7 years ago
Joachim Klein
2948611f3f
cli.cpp: Quote arguments in "Command line arguments" status line
It's nice to be able to copy-paste the arguments from a log file to a shell,
so we'd like to have proper quoting.
We thus use single quotes if an argument contains non-safe characters
in the log output.
7 years ago
Joachim Klein
04a1bbedfc
properties.cpp: Log filename of properties file in --verbose mode
7 years ago
Joachim Klein
30a95ef9d6
Simplify check whether argument of --prop is a file/property
Before, the argument to `--prop` was only treated as a file if (a) it exits and (b) contains a dot.
We remove the requirement for a dot and always treat the argument as a file if it exists.
7 years ago
dehnert
9b80c65d72
more and more debugging
7 years ago
Alexander Bork
fa43e515ee
Changed DFT element transformation so priorities are used
7 years ago
dehnert
135c38777f
game-based abstraction working with rational numbers
7 years ago
dehnert
14724b529f
further debugging
7 years ago