7bcf78650f
Included missing header required to output boost::optionals in tests
4 years ago
3af128184e
Fixed usage of missing operator<< for permissive scheduler tests
4 years ago
0d43a55923
Fixed incorrect type of modulo expression with integer inputs
4 years ago
f0378363bb
ConstantsComparator: reduced code duplications, fixed a potentially div by 0, and silenced a warning
ConstantsComparator: The old code used `abs(x-y)/abs(x+y)<= epsilon` when comparing two numbers for equality (modulo relative precision). This is weird when x and y have different signs and potentially even causes a div by 0 whenever x=-y. Moreover the templating was awkward, causing a lot of code duplications and a Warning with clang.
Distribution[WithReward]: replaced forward declarations of ConstantsComparator by actual includes as the forward declarations caused some ambiguity regarding the template parameters.
4 years ago
c5bbf68eaf
Removed several unnecessary forward declarations of ConstantsComparator.
4 years ago
bdd89d87b2
Prism next state generator now deals with unbounded integer variables.
4 years ago
1fe0254f5d
DdPrismModelBuilder now errors in case it has a program with unbounded integer variables as input
4 years ago
9f1c540f05
Counterexamples:making minimal label set generator aware of unbounded integer variables
4 years ago
171ff270e0
Prism to Jani conversion now supports unbounded integer variables
4 years ago
8f9ff95531
Added Test cases for parsing/processing prism programs that use unbounded integer variables
4 years ago
5c2b9c503c
prism/Program: Integer variables can now have no lower and/or upper bound.
4 years ago
aa5bb9cb7d
PrismParser: Parsing unbounded integer variables
4 years ago
871efc0d8c
Fixed TerminalStatesGetter with multi-bounded formulae.
4 years ago
c3859ec021
Add merge operation to RelevantEvents
4 years ago
8bccb7ffa1
Fix const correctness in RelevantEvents
4 years ago
7cd2394078
Make RelevantEvents independent of std::vector
Instead use a flexible iterator based api
4 years ago
d5c6a509a2
JaniNextStateGenerator: Fixed evaluation of terminal states using expressions over transient variables
4 years ago
95d53e444b
Fixed an issue with jani::VariablSet using different kinds of variable names when adding and deleting variables.
4 years ago
66e6938d20
added a few clarifying comments in JaniNextStateGenerator
4 years ago
168b5fabd6
Silenced several warnings
4 years ago
45a7db8222
LpMinMaxLinearEquationSolver: Fixed an issue when using glpk occurring when the lower bound of a variable matches the upper bound. Also revamped retrieving of lower/upper bounds.
4 years ago
e59918668e
AbstractEquationSolver: Added more convenient getters for the most appropriate lower/upper bound of a given variable
4 years ago
6df0efcd3e
Set result correctly for reachability rewards in MdpInstantiationChecker
4 years ago
eaff65ef27
LinearCoefficientVisitor: Fixed translation of division expressions.
4 years ago
9fea07542a
Fixed warning
4 years ago
c9841b71a0
Const reference for splittingThreshold
4 years ago
8d17a0362d
Fix extremal value computation
4 years ago
0ed64b6257
Add == and != ops to RelevantEvents
and simplify constructor of RelevantEvents
4 years ago
7a2b060afc
Remove allowDCForRelevant from RelevantEvents
4 years ago
972ef8b14c
Break inclusion loop in DFT.h
and comment magic numbers in RelevantEvents.h
4 years ago
7fc4046fbc
Fix DftSimulatorTest for older Boost versions
4 years ago
76afd5e3de
Implemented basis for handling invalid traces during simulation
4 years ago
6eec25de6c
Typos
4 years ago
7111674ec8
Support for simulation of PDEP
4 years ago
9e3e2c02fe
Handle PDEP in createSuccessorState as well
4 years ago
6c025f13d2
Added more tests for DFT simulation
4 years ago
344ba353e0
Use template for DFTTraceSimulator
4 years ago
fb2f55d804
Fixed bug where POR was changed to PAND during transformation to binary FDEPs
4 years ago
6d24ea9606
Silenced many 'loop variable is always a copy' warnings
4 years ago
481d23b904
Replaced storm::expressions::Expression::operator^ by storm::expressions::pow. An optional flag indicates if we should allow power expressions of integer type (PRISM semantics) or whether it is always a real (JANI semantics).
4 years ago
46462d6556
Z3Adapter: Fixing translation of XOR operators - expression's operator^ is supposed to be power, not xor.
4 years ago
d863fe4156
Jani Export: Power expressions of integer type need to be type casted.
4 years ago
94cd2e7fbd
Apply rewriting only for modularisation
4 years ago
5a37a40cea
Monotonicity for computing extremal value and parameter space partitioning
4 years ago
868c9fb0fd
Fixed activation for failed nested SPAREs.
If a nested (passive) SPARE is already failed and it becomes activated (through claiming), it will not activate its children.
4 years ago
e156d7b8e7
Prevent problems with different random values on older Boost versions
4 years ago
5b053fa59c
Tests for DFT simulator
4 years ago
54e665aff1
First version of simulator for failure traces in DFTs
4 years ago
d6d36ee557
Support for sampling from exponential distribution
4 years ago
656e823287
Refactored DFT Api Test
4 years ago
Tim Quatmann
Johannes Lehmann
Daniel Basgöze
Matthias Volk
Jip Spel