Tim Quatmann
8a23197a77
Fix for LRA scheduler generation.
5 years ago
Tim Quatmann
72425ec1b2
CLI: Added an option to export the produced scheduler to a file.
5 years ago
Tim Quatmann
009cee1c25
Implemented scheduler extraction for LRA properties for MDP.
5 years ago
Tim Quatmann
c1b3a4f991
LraMdpPrctlModelCheckerTest: Test LRA computation for different environments. Added a testcase.
5 years ago
Tim Quatmann
48dbaa6fbd
Fixed a test
5 years ago
Tim Quatmann
16aee7c386
fixed a typo
5 years ago
Matthias Volk
9e63a89db7
Fixed operator precedence for power and modulo operator thanks to help from Joachim Klein.
5 years ago
Matthias Volk
d05b132dde
Better error output
5 years ago
Tim Quatmann
900da9e556
Fixed EndComponentEliminatorTest
5 years ago
Tim Quatmann
2cb7b5769e
Jit: Fixed issues when CLN and/or GMP is installed via carl
5 years ago
Tim Quatmann
b1b429e8d2
EndComponentEliminatorTest: Made the test more stable with respect to different orders in the result.
5 years ago
Jip Spel
b308f4e1d0
Initialize region before creating sample points
5 years ago
Jip Spel
12e0ef537c
Small fixes
5 years ago
Tim Quatmann
492348542f
SubsystemBuilder: Fix deadlocks with a selfloop (if requested)
5 years ago
Tim Quatmann
0b1b0d97e2
utility/graph: fixed behavior of getReachableStates when an initial state is not in the constrained set.
5 years ago
Jip Spel
e0b2869bd5
Fix region check
5 years ago
Jip Spel
08d2893b2c
Renamed Lattice -> Order
5 years ago
Jip Spel
1c5d6b7237
Clean up lattice creation code
5 years ago
Jip Spel
8214c5758e
Use parameter lifting for initial ro construction
5 years ago
Alexander Bork
adf07416dc
Added preservation of time bounded until formulae
5 years ago
Tim Quatmann
b848796852
Nativepolytope: Fixed a bug in quickhull when invoked on just a single point.
5 years ago
Matthias Volk
174c1a86c0
DRNParser: Parse labels with and without quotation marks (thanks to pair programming and regex magic
5 years ago
Matthias Volk
779e5ce5ae
DRNParser: Check if target state is valid
5 years ago
Sebastian Junges
976f85cc25
drn export for labels with whitespace is now put into quotation marks
5 years ago
Alexander Bork
450e074c5b
Integrated non-Markovian state elimination into Storm MA modelchecking
5 years ago
Alexander Bork
7b038db6d5
Fixed missing part for label preservation and added formula preservation check
5 years ago
Sebastian Junges
31b50d76e9
clearer error message
5 years ago
Sebastian Junges
3efee0d35d
changelog update: export of mtbdds
5 years ago
Sebastian Junges
9ad8209a65
clarify that a formula needs to be added to do anything in storm-pomdp
5 years ago
Alexander Bork
a73c2691b6
Integration of the new settings in the DFT analysis
5 years ago
Alexander Bork
5aa19c9a58
Added settings for non-Markovian state elimination
5 years ago
Alexander Bork
88d6300084
Added option for label preservation to state elimination
5 years ago
Sebastian Junges
f5b6bc84ba
circumvent problems with the bdd export
5 years ago
Sebastian Junges
4f063cd233
tackling problems on unix
5 years ago
Matthias Volk
6ce429efc4
Added missing include
5 years ago
Jip Spel
13f44ab7ea
Monotonicity Checking on Region
5 years ago
Alexander Bork
ec67166041
Decoupled preprocessing and SMT solving in commandline interface
5 years ago
Alexander Bork
449c513db2
Cleanup DFTASFChecker
5 years ago
Alexander Bork
75d28060cc
Moved failure bound computation to decouple it from the SMT checker
5 years ago
Sebastian Junges
85e995c050
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
5 years ago
Sebastian Junges
d295f6e777
export of bdds into dot and text format
5 years ago
Alexander Bork
9c74bbed24
Decoupled FDEP conflict search and SMT solver
5 years ago
Alexander Bork
ae5c001d24
Moved non-Markovian state eliminator to its own class
5 years ago
Alexander Bork
2709b7d828
Merge branch 'master' into dftFDEP
5 years ago
Alexander Bork
10bb42e0f6
First version of non-Markovian state elimination for MAs
5 years ago
Matthias Volk
9c52d0d2ab
Workaround for IntelTBB linker issue by CMake/Regex magic.
IntelTBB does not use symlinks (as commonly used) to reference its libraries but instead uses linker scripts.
These linker scripts do not work with GCC and linking fails.
As a workaround we manually set the correct library in CMake after extracting the path from the linker script with regex magic.
This workaround is highly hackish and might break in the future.
5 years ago
Matthias Volk
7fb660227f
Replaced assert(false) by throwing an exception
5 years ago
Matthias Volk
685b5c6b27
Throw exceptions after switch/case to silence compiler warnings about not returning anything
5 years ago
Matthias Volk
adfe82d0d6
Fixed typo to void
5 years ago
Tim Quatmann
230a2c86d3
Mentioning QVBS as Benchmark source in README
5 years ago