Jan Erik Karuc
323e82994d
maixmumElementDiff implementation in vector.h
5 years ago
Sebastian Junges
0a6f54f33e
a version of parsing choice labels from DRN
5 years ago
Sebastian Junges
f322149398
export the number of choices into drn
5 years ago
Sebastian Junges
a58ec3fd5f
permutations for vectors
5 years ago
Matthias Volk
ee3c08a085
Set floating-point precision to 10 digits for file export
5 years ago
Matthias Volk
729dda163d
Fixed export in DRN format: parameters could occur multiple times
6 years ago
Tim Quatmann
99991d344e
utility/initialize: Added a function to read the current loglevel.
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
8b77f7f6d6
Added placeholders to DRN format
6 years ago
Tim Quatmann
429c91ff13
Added support for parsing fractions in DRN files.
6 years ago
Tim Quatmann
0b1b0d97e2
utility/graph: fixed behavior of getReachableStates when an initial state is not in the constrained set.
6 years ago
Sebastian Junges
976f85cc25
drn export for labels with whitespace is now put into quotation marks
6 years ago
Sebastian Junges
f5b6bc84ba
circumvent problems with the bdd export
6 years ago
Sebastian Junges
4f063cd233
tackling problems on unix
6 years ago
Matthias Volk
6ce429efc4
Added missing include
6 years ago
Sebastian Junges
d295f6e777
export of bdds into dot and text format
6 years ago
Matthias Volk
7fb660227f
Replaced assert(false) by throwing an exception
6 years ago
Matthias Volk
685b5c6b27
Throw exceptions after switch/case to silence compiler warnings about not returning anything
6 years ago
Matthias Volk
6a4c18e4a2
Use custom FlatSet to account for allocator changes in flat_set in Boost 1.70.
Boost 1.70 changed the default allocator parameter from new_allocator<T> to void to reduce symbol lenghts.
This reverts the default to the old allocator.
6 years ago
TimQu
bb0c2282b3
Fixed levenshtein distance
6 years ago
TimQu
8807bb5a0b
Settings: Added facilities to flag options as advanced and only display them with '--help all'.
6 years ago
TimQu
e8cd922552
utility/string.h: Added method to check whether a string is considered similar.
6 years ago
Tim Quatmann
b4f652bbc8
Reducing the nesting when creating a expression::sum(...).
6 years ago
Tim Quatmann
b70f28b10e
Ensured that utility function for rounding always rounds towards infinity.
6 years ago
Tim Quatmann
a34037bff4
Added utility function for rounding.
6 years ago
Tim Quatmann
3a11a4b3eb
Introducing a TBB adapter that #undefs TRUE and FALSE.
6 years ago
Tim Quatmann
dd1d53046c
utility/constants.cpp: Fixing unknown 'isnan'
6 years ago
Tim Quatmann
3836fd42c0
utility/vector: Added hasZeroEntry and hasInfinityEntry
6 years ago
Tim Quatmann
4322d00034
FilteredRewardModel: added create method that works without a checkout.
6 years ago
Tim Quatmann
3a21ce8009
utility/vector: buildVectorForRange now gets the type of the vector as a template parameter.
6 years ago
TimQu
c7aec92dc9
modelchecker: Added support for non-trivial reward accumulations for Sparse/Hybrid/Dd engines.
6 years ago
Tim Quatmann
5869a1f5fd
Simplified StronglyConnectedComponentDecomposition.
6 years ago
Matthias Volk
b9c38fe11a
Fixed includes
6 years ago
Tim Quatmann
5d57746db2
If an option is unknown, Storm now prints a hint to similar option names.
6 years ago
Tim Quatmann
01800f1590
Added string utility functions to find similar strings.
6 years ago
Tim Quatmann
27c2a8ba95
Added string utility functions to find similar strings.
6 years ago
Tim Quatmann
c6fd015e6c
Picking a default SmtSolver, even if no CoreSettings are available.
6 years ago
Tim Quatmann
84476b7000
Fixed getSmtSolver which previously did not respect the SmtSolver selection from the settings.
6 years ago
TimQu
e89cbf2886
fixed cyclic check.
6 years ago
TimQu
04082fb2d6
Added a method to check whether a graph contains a cycle.
6 years ago
TimQu
4924a0e557
Fixed 'isZero' function in ConstantsComparator.
7 years ago
Sebastian Junges
43688d09ea
reward infinity scheduler extraction is now correct
7 years ago
Sebastian Junges
93ca559c83
additional sanity checks for scheduler extraction
7 years ago
TimQu
e6fc962e5e
In exact mode, use LP as LRA Method for nondeterministic models.
7 years ago
sjunges
d417c9ecbe
Fix assertion. assert(x < y < z) is not the same as assert(x < y and y < z).
7 years ago
Sebastian Junges
fef4b694d4
topo sort: add first states
7 years ago
TimQu
4dc234d635
silenced several 'unused parameter'-warnings
7 years ago
TimQu
ea1a1d97ef
fixed export of jani functions to json. Remove output to cout when writing the jani file
7 years ago
TimQu
034fbf20c7
extended SubsystemBuilder, made ChoiceSelector work for MAs as well.
7 years ago