TimQu
11b9c60515
Adapted fragment checker test to new multiobjective-fragment specification
9 years ago
TimQu
9591157996
new features for storm-pars api:
- depth limit for iterative refinement
- the regions with inconclusive result are now also part of the result
- when analyzing a region, a hypothesis (AllSat or AllViolated) can now be given
9 years ago
Sebastian Junges
980f1864af
test cases
9 years ago
TimQu
bb897a94c6
Moved ModelInstantiatorTest to storm-pars
9 years ago
TimQu
4191d17f1e
Moved main testfiles into tests/storm/ and the storm-pars testfiles into tests/storm-pars
9 years ago
TimQu
2f49255db6
Improved storage::Scheduler. We can now consider arbitrary finite memory schedulers, potentially employing randomization.
9 years ago
dehnert
2794de2342
added missing include to make gcc happy
9 years ago
TimQu
35c9b58fda
added a test case for SparseMatri::restrictRows and fixed it
9 years ago
Matthias Volk
ac566a64c3
Removed some whitespace
9 years ago
dehnert
179cd8308e
remove old API files
9 years ago
dehnert
ea02ea0838
started overhaul of cli/api
9 years ago
TimQu
0cdd32ff9f
added two test cases for the drn parser
9 years ago
TimQu
e7a8357ee6
Fixed some tests
9 years ago
TimQu
88fc7fda0c
fixed tests that used the prism model builder (reverted from commit f762491ce4)
9 years ago
TimQu
576f92568e
StateValuations and ChoiceOrigins are now members of a sparse::Model.
A model can now be constructed by providing a modelComponents struct.
9 years ago
TimQu
722e67fe64
parsing choice labels for explicit models
9 years ago
TimQu
f558cb866c
using exact data types for smt-based multi objective model checking tests. Also disabled a few tests that test (yet) unsupported queries or that take too long.
9 years ago
TimQu
6537fd8b72
Replaced the old choice labeling with the new one and used choice origins for the minimal command set counterexample generators
9 years ago
dehnert
70ebe36ec6
adapted tests to recent changes wrt to 0-transition insertions in explicit parser
9 years ago
TimQu
f762491ce4
fixed tests that used the prism model builder
9 years ago
TimQu
25074b50a9
Added function to get the next unset bit in a bitvector
9 years ago
TimQu
1c768c1ceb
constraint based tests for multi-obj MAs
9 years ago
TimQu
5c338b0092
added missing file extension
9 years ago
TimQu
b8229da6cd
disabled quantitative query tests for constraint based checking
9 years ago
TimQu
aa4d2141c3
build infrastructure for switching between multi objective model checking methods
9 years ago
dehnert
03ad4c2783
first version of symbolic bisimulation minimization
9 years ago
TimQu
a896c0df28
improved exact computations
9 years ago
TimQu
ee754c96e2
renamed ParameterLifting.h -> RegionChecker.h
9 years ago
TimQu
2647ffa9ae
added test for exact validations
9 years ago
TimQu
d659d193bc
Fixed game solver test and potential memory leaks
9 years ago
dehnert
853b035473
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
9 years ago
dehnert
153339c5be
first draft of policy iteration using DDs
9 years ago
dehnert
952776a057
hybrid engine working for rational numbers
9 years ago
dehnert
ee90c51b2a
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
9 years ago
dehnert
aaa6f13cf4
separated rational numbers and rational functions and added support for rational numbers to sylvan
9 years ago
TimQu
7f74f19342
exact pla
9 years ago
dehnert
0354c9024a
moved to new sylvan version and made everything work again
9 years ago
TimQu
8212cadf00
adapted changed filename in test
9 years ago
TimQu
c4dffe9a8b
tests for step bounded properties
9 years ago
TimQu
24bc53549c
more tests on pmdps and fixes
9 years ago
dehnert
a323d21751
fixed some wrong capitalization
9 years ago
TimQu
1e1b037cb2
minor fixes
9 years ago
TimQu
38fa454ace
fixed more compilation issues, considered the variables occurring in the model when parsing a region (otherwise, distinct variables with the same name would cause problems), adapted Tests to new interface for parameter lifting
9 years ago
TimQu
14e44e0165
removed old region model checker classes, implemented entry point for pla, solved different compilation issues
9 years ago
TimQu
536b1669c3
fixes for dtmc parameter lifting
9 years ago
Tom Janson
a22ec04f10
fix old KSP test include
actually still works fine
9 years ago
TimQu
e2606e7b8c
only do z3 optimizer tests if z3::optimize is available
10 years ago
TimQu
4081e4bfbe
removed debug output and fixed a test
10 years ago
TimQu
1d2e7b2450
compilation fixes
10 years ago
dehnert
dd137d6479
added test for using actions multiple times in different synch vectors in JANI model (DD builder)
10 years ago