Matthias Volk
174c1a86c0
DRNParser: Parse labels with and without quotation marks (thanks to pair programming and regex magic
6 years ago
Matthias Volk
779e5ce5ae
DRNParser: Check if target state is valid
6 years ago
Sebastian Junges
976f85cc25
drn export for labels with whitespace is now put into quotation marks
6 years ago
Alexander Bork
450e074c5b
Integrated non-Markovian state elimination into Storm MA modelchecking
6 years ago
Alexander Bork
7b038db6d5
Fixed missing part for label preservation and added formula preservation check
6 years ago
Sebastian Junges
31b50d76e9
clearer error message
6 years ago
Sebastian Junges
9ad8209a65
clarify that a formula needs to be added to do anything in storm-pomdp
6 years ago
Alexander Bork
a73c2691b6
Integration of the new settings in the DFT analysis
6 years ago
Alexander Bork
5aa19c9a58
Added settings for non-Markovian state elimination
6 years ago
Alexander Bork
88d6300084
Added option for label preservation to state elimination
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
Jip Spel
13f44ab7ea
Monotonicity Checking on Region
6 years ago
Alexander Bork
ec67166041
Decoupled preprocessing and SMT solving in commandline interface
6 years ago
Alexander Bork
449c513db2
Cleanup DFTASFChecker
6 years ago
Alexander Bork
75d28060cc
Moved failure bound computation to decouple it from the SMT checker
6 years ago
Sebastian Junges
d295f6e777
export of bdds into dot and text format
6 years ago
Alexander Bork
9c74bbed24
Decoupled FDEP conflict search and SMT solver
6 years ago
Alexander Bork
ae5c001d24
Moved non-Markovian state eliminator to its own class
6 years ago
Alexander Bork
10bb42e0f6
First version of non-Markovian state elimination for MAs
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
adfe82d0d6
Fixed typo to void
6 years ago
Alexander Bork
549774abc9
Added state remapping in state elimination
6 years ago
Alexander Bork
27e65d5669
Added construction of the state remapping for elimination of non-Markovian states in MAs
6 years ago
Alexander Bork
add2a40a62
Integrated results of FDEP conflict search in DFT state space generation
6 years ago
Tim Quatmann
b357868a32
GurobiLpSolver: Fixed rounding of integral results.
6 years ago
Matthias Volk
47344f9080
Removed unused flat_set includes
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
Matthias Volk
1e3686480a
is_equal_to_one() is not used in Boost 1.70
6 years ago
Alexander Bork
3616bdbf13
Added two test cases for the FDEP conflict search
6 years ago
Alexander Bork
e2ef6bc52a
Added missing initialization of result vector
6 years ago
Alexander Bork
589555c75f
Moved dynamic behavior computation from builder to DFT and added SEQ and SPARE cases
6 years ago
Jip Spel
6db964363e
Update for artifact evaluation ATVA
6 years ago
Jip Spel
4a1f98a0ba
Fix segfaults
6 years ago
Matthias Volk
84467267e0
Second try to improve performance for relevant events
6 years ago
Alexander Bork
aa150fc2e3
Extended FDEP conflict search by not considering pairs of FDEPs with static behavior
6 years ago
Alexander Bork
bec75813b1
Added computation of dynamic behavior vector for DFTs
6 years ago
Alexander Bork
39ec751f8d
Removed debugging output
6 years ago
Matthias Volk
187d47d8ac
Try to improve performance for relevant events
6 years ago
Alexander Bork
9bfc7858d0
Added improved upper bound correction
6 years ago
Alexander Bork
583a880620
Adjusted DFT to SMT conversion to deal with constant failures
6 years ago
Alexander Bork
a0c42fa630
Added debugging messages for transformations
6 years ago
Matthias Volk
d0494d07e6
Get settings only once for takeFirstDependency
6 years ago
Tim Quatmann
bc623d1203
MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler.
Renamed the 'hasNoEndComponents' solver requirement to 'hasUniqueSolution' as this is the actual thing we require for, e.g. sound value iteration.
6 years ago
Matthias Volk
820b48354d
Silenced warning
6 years ago
Matthias Volk
9c28ed990e
Use isBasicElement() instead of type
6 years ago
Matthias Volk
51b210a1d6
Test case for symmetry reduction
6 years ago
Matthias Volk
08859bd3e6
Fixed bug in computation of symmetry groups.
Thanks to Enno Ruijters for pointing out this issue.
6 years ago