dehnert
|
0fed84c5a9
|
removed superfluous return
|
8 years ago |
Matthias Volk
|
db32a91c7c
|
Changed logging level for some output
|
8 years ago |
|
dehnert
|
316412c5d3
|
fixed a bug related to closing symbolic Markov automata
|
8 years ago |
|
dehnert
|
09866e4577
|
enabling changing value type in quotient extraction of dd-bisimulation
|
8 years ago |
|
dehnert
|
139752eb66
|
added option to perform dd-bisimulation using exact arithmetic
|
8 years ago |
|
dehnert
|
8482063a16
|
made symbolic bisimulation work with MA and support of sparse quotient extraction for MA
|
8 years ago |
|
dehnert
|
9e5e1980dd
|
first working version of symbolic Markov automaton bisimulation
|
8 years ago |
TimQu
|
a1c10cac37
|
filtering reward zero states for MDPs
|
8 years ago |
|
dehnert
|
4591dba631
|
made maxsat-based counterexample generation be applicable to DTMCs and MDPs
|
8 years ago |
|
dehnert
|
676120229b
|
intermediate stage
|
8 years ago |
|
dehnert
|
0d18886966
|
re-enabling conversion of MA to CTMC if the MA only has Markovian states
|
8 years ago |
Joachim Klein
|
f56076aacf
|
Add virtual destructors to classes having virtual functions.
(Silences warnings from -Wdelete-non-virtual-dtor -Wnon-virtual-dtor)
|
8 years ago |
|
dehnert
|
41828ca27d
|
more work on bisimulation-based abstraction-refinement
|
8 years ago |
|
dehnert
|
9c685f3bdb
|
started on partial bisimulation model checker
|
8 years ago |
|
Matthias Volk
|
4456069e81
|
Fixed typo
|
8 years ago |
|
Matthias Volk
|
88544a9ec7
|
Added assertion for turnRatesToProbabilities in MA
|
8 years ago |
|
Matthias Volk
|
983e09fd63
|
Fixed possible problem with rates and exit rates in MA
|
8 years ago |
|
dehnert
|
55c787e0d8
|
proper EC elimination in hybrid helper
|
8 years ago |
|
TimQu
|
fcd277c42a
|
added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format
|
8 years ago |
|
dehnert
|
3c844a487f
|
some more optimizations
|
8 years ago |
|
TimQu
|
999fd0752c
|
The model memory product can now retrieve the reachable states without actually building the product
|
8 years ago |
|
TimQu
|
76c01de25c
|
use utility::vector::max_if to compute the maximum exit rate in an MA
|
8 years ago |
|
TimQu
|
8efccd76d2
|
started to make multi-objective preprocessing more flexible w.r.t. different checkers
|
8 years ago |
sjunges
|
b120b74fa9
|
StateActionPair to index should be part of nondeterministicmodel
|
8 years ago |
|
sjunges
|
6e506e5a66
|
moved application of permissive scheduler to an own transformer
|
8 years ago |
|
dehnert
|
ad456916e9
|
first working version of sparse reward model quotienting
|
8 years ago |
|
dehnert
|
722cb3109c
|
dd quotient extraction of reward models in dd bisimulation
|
8 years ago |
|
dehnert
|
34e23f94fc
|
started on reward model preservation in DD bisimulation
|
8 years ago |
|
dehnert
|
f96403de9e
|
added reduction to state-based rewards to symbolic (reward) models
|
8 years ago |
|
dehnert
|
d23547d99f
|
started optimizing some DdManager methods
|
8 years ago |
|
dehnert
|
2b0911d627
|
more work on MDP bisimulation
|
8 years ago |
|
dehnert
|
a1db269e8f
|
started on debugging MDP bisimulation
|
8 years ago |
|
dehnert
|
f3ebfaa90f
|
more work on MDP bisimulation
|
8 years ago |
|
dehnert
|
b25ef3f09c
|
introduced symbolic bisimulation modes lazy and eager, fixed bug in sparse quotient extraction
|
9 years ago |
|
TimQu
|
e8e189723f
|
fixed applying memoryless schedulers
|
9 years ago |
|
TimQu
|
5651b23771
|
fixing minor compiling issue
|
9 years ago |
|
TimQu
|
a348f6ea8e
|
function to apply a given scheduler to a nondeterministic model
|
9 years ago |
|
TimQu
|
19925ac74d
|
implemented value iteration based Long run average rewards for Markov automata by Butkova et al. (TACAS 2017)
|
9 years ago |
|
dehnert
|
ea02ea0838
|
started overhaul of cli/api
|
9 years ago |
|
TimQu
|
e7a8357ee6
|
Fixed some tests
|
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 |
|
dehnert
|
f0f4cd7390
|
first version of sparse quotient extraction for dd bisimulation
|
9 years ago |
|
TimQu
|
464bdc389c
|
improved state valuations class
|
9 years ago |
|
TimQu
|
722e67fe64
|
parsing choice labels for explicit models
|
9 years ago |
|
TimQu
|
1d329176ba
|
Resolved compiling issues due to recent merge
|
9 years ago |
|
TimQu
|
cd5ee63cce
|
fixed preserving the choice labeling when an ma is closed
|
9 years ago |
|
TimQu
|
b531dccad9
|
.dot output for deterministic models with choice labels
|
9 years ago |
|
TimQu
|
e7bc5fdef9
|
fixed several minor bugs regarding the choicelabeling
|
9 years ago |
|
TimQu
|
bf97d79573
|
moved building the choice origin strings into the ChoiceOrigins class
|
9 years ago |
|
TimQu
|
db31c1cb11
|
improved .dot export of models with choice labeling
|
9 years ago |
