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
9 years ago
TimQu
4081e4bfbe
removed debug output and fixed a test
9 years ago
TimQu
1d2e7b2450
compilation fixes
9 years ago
dehnert
dd137d6479
added test for using actions multiple times in different synch vectors in JANI model (DD builder)
9 years ago
TimQu
f01e48644e
fixes for nativepolytopes
9 years ago
dehnert
e6bf0339d3
overhaul of JANI model building to allow using actions of automata in several synchronization vectors
9 years ago
TimQu
4642ed23be
enable pcaa tests when hypro is not available
9 years ago
Matthias Volk
5d79eff2cd
Wrapper for file opening
9 years ago
dehnert
9c581bd635
fixed two issues: missing include in ToRationalNumberVisitor and missing check for whether actions are reused in a JANI parallel composition
9 years ago
TimQu
ed465f75bd
added Z3LPSolver
9 years ago
dehnert
a85f4fdc89
replaced some StoRMs and Storms by storm, reworked version output a bit
9 years ago
dehnert
77bd6e4a44
fixed some model building issues
9 years ago
dehnert
aac7433f39
expression manager now caches types, expression evaluator avoid creating unnecessary expressions and traversals
9 years ago
TimQu
18dac3231e
.... actually fixed pcaa tests
9 years ago
dehnert
ad18fee1dc
commit to switch workplace
9 years ago
TimQu
f02ffd9d5b
fixed pcaa tests
9 years ago
TimQu
6eeae9ed9b
fixed pcaa tests
9 years ago
dehnert
16a06d9f03
formula parser now directly emits properties with names; name filtering of properties from cli
9 years ago
dehnert
b4381a7c48
Constants in formulas appear to be working
9 years ago
dehnert
cb8b537baa
made storm compile again with expressions in time-bounds of until formula
9 years ago
Sebastian Junges
d2c658f6c1
removed deprecated expectation in test
9 years ago
Sebastian Junges
e4de643b0f
disabled two tests which indicate problems which are about to be fixed in a different way
9 years ago
Sebastian Junges
941afa46bc
removed windows specific code
9 years ago
dehnert
61157cc1c5
add warning when computing minimal rewards on MDPs that reward values may be too low
9 years ago
Sebastian Junges
3b4b5e3a38
disable tests which depend on mathsat if mathsat is not available, gives a warning in verbose output
9 years ago
Sebastian Junges
3795519fea
removed old unit tests for jani parser, to be replaced by regression tests
9 years ago
TimQu
c1063f27cc
added a few more tests for multi-objective MAs. Also fixed/improved minor stuff.
9 years ago
dehnert
56d1928b9b
resolved some issues (ambiguity for call to carl::rationalize and several warnings because of signed/unsigned comparison)
9 years ago
Sebastian Junges
1d8c5f26a4
make tests builds all tests without running them. Make check now again works with the new location for executables
9 years ago
TimQu
fb54edfb11
adapted pcaa tests to recent interface changes
9 years ago
TimQu
83a77e77ba
fixed use of gmp numbers
9 years ago
TimQu
ae3ef2f14a
added testfiles for multiobjective mc tests
9 years ago
dehnert
a976352b8c
some fixes to make tests pass
9 years ago
dehnert
b258f1e52d
some more warnings gone
9 years ago
dehnert
5b09b91ae1
fixed more warnings
9 years ago
dehnert
bc5dd814aa
fixed some tests
9 years ago
Tom Janson
b71ef02692
comments and fixes (?) to graph.cpp's Dijkstra
This implementation seemed pretty wrong in multiple ways;
I attempted to fix it (a long time ago) (see diff, you'll see what I'm
talking about), then gave up.
Luckily (?) the code is unused, just sitting there, sad and broken.
9 years ago
Tom Janson
87e8af9852
moved ksp stuff to right location
fix include
9 years ago
dehnert
9bb65389c4
some adjustments to pgcl treatment caused by changes in JANI data structures
9 years ago
tomjanson
b89d3f289a
group targets & minimal paths
Note that this is a major, API-breaking change.
Also bunched into this commit:
- rename namespace `shortestPaths` to `ksp`
- omit unneeded namespace qualifiers
- move tests from `GraphTest` to `KSPTest` and wrote more
- path representation explanation in .md file
Former-commit-id: f395c3df40
[formerly 7fa07d1c8f
]
Former-commit-id: f50dd3ce7c
10 years ago
tomjanson
d8f2eec9af
actual test for single-target non-disjoint KSP
Former-commit-id: abb27b9078
[formerly 8492e75c07
]
Former-commit-id: c60c829826
10 years ago
tomjanson
140597fb90
interactive debug in test
Former-commit-id: 161afac16e
[formerly 17962bf200
]
Former-commit-id: 53dc4819cf
10 years ago
tomjanson
df195d85f6
REA fully implemented; needs testing
Former-commit-id: 9795a24835
[formerly fc732962dd
]
Former-commit-id: 0ae2abacd1
10 years ago
tomjanson
38d22093a3
documentation / cleanup
Former-commit-id: e7798a5669
[formerly 43dd865fbc
]
Former-commit-id: 6fb69a017c
10 years ago
tomjanson
010f0ca988
shortest paths generator skeleton
Former-commit-id: c37fdbbec8
[formerly 23dba537c7
]
Former-commit-id: 6eb54e64ad
10 years ago
sjunges
2aec312fbd
testcase-stub for kshortest added
Former-commit-id: 215c5b7378
[formerly 5598231acb
]
Former-commit-id: 6d51229aa1
10 years ago