TimQu
87e34d7b32
Added Support for Total Reward Formulas for DTMCs in the Sparse Engine
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
Matthias Volk
a6e6d5993f
Travis: set unlimited clone depth to allow versioning with git describe
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
sjunges
8478352030
dynamic constraints and minimality labels
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
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
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
Matthias Volk
a2c990ea58
Travis: changed mail address for notifications
7 years ago
Matthias Volk
c5e356bc40
Proper installation of Storm
7 years ago
Matthias Volk
99e5619952
Export storm targets
7 years ago
TimQu
1e4b81812c
Environment does no longer require that unused setting modules still have to be registered.
7 years ago
TimQu
5c38a4ef89
implemented environment for multiobjective settings
7 years ago
dehnert
e1bb35ca0f
fix for the generator matrix fix
7 years ago
dehnert
62e493d978
fix computation of generator matrix, pointed out by jklein
7 years ago
dehnert
ca651ec61c
fixes github issue #24 related to MEC decomposition
7 years ago
dehnert
03707f0234
first step for fixing MEC decomposition: making SCC decomposition accept a bit vector of subsystem choices
7 years ago
dehnert
94a5a3da7c
remove ffast-math
7 years ago
Matthias Volk
2ba70e964c
Added hasParameters() and supportsParameters() for symbolic models
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
dehnert
ceea5198d6
fixed detection of unreachability of target state in MaxSAT-based high-level counterexample generation
7 years ago
Sebastian Junges
e7926b10c2
allow counterexamples for true jani models
7 years ago
Sebastian Junges
c517ec14b1
support for liveness cex in jani
7 years ago
Sebastian Junges
0726dfc7a0
bugfix only add label out of bounds is option is set and state is present
7 years ago
Matthias Volk
e6090d2d2c
Removed unused code
7 years ago
Sebastian Junges
5b6383b5ef
fix gspn export to pnml
7 years ago
Sebastian Junges
7a2a46cae9
fix warning about non-const comparison operator in set
7 years ago
Sebastian Junges
89f3aac33f
add error messages for sparse model building when lower bounds for variables are above upper bounds
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
Sebastian Junges
d77f4e7564
gspn pnml export for capacities
7 years ago
Sebastian Junges
61f31fb919
improved handling of capacities by switching to boost::optional
7 years ago
Sebastian Junges
1c9f7b0f2f
translate prism to jani with a suffix for location names etc when doing this for multiple models
7 years ago
Sebastian Junges
33ac2e0793
make jani models copyable
7 years ago
Sebastian Junges
56df741d32
formula parser does not depend on jani model
7 years ago
Sebastian Junges
687bb0dd86
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
7 years ago
Sebastian Junges
fdcbd6369c
simple sanity check for bounded integers in jani
7 years ago