Lukas Posch
5473966cd1
changed clippedStatesOfCoalition with size and values from relevantStates
4 years ago
Lukas Posch
318544a940
refactor computation of relevantStates from BitVector method to logical AND
4 years ago
Lukas Posch
781f105ca1
introduced name relevantStates,
moved methods to Bitvector class
4 years ago
Sebastian Junges
0a5717aee7
lowlevel storing/loading bitvectors from a string (without any error handling, that is). Helpful to store bitvecots in python
5 years ago
Matthias Volk
9fc473383f
Cosmetic changes in BitVector.
Pro: Better documentation, fewer compiler warnings.
Contra: Recompilation of 400 files.
5 years ago
Sebastian Junges
7bebb18250
bitvector concat and expand
5 years ago
Sebastian Junges
0dd15b4e2f
permute for bitvectors
5 years ago
Tim Quatmann
004466b83f
Fixed BitVector::full() for BitVectors with size 0
6 years ago
dehnert
95fae73833
slight improvements to bit vector hashmap
8 years ago
dehnert
8b557c36a7
adding murmur3 as a possible hash fct for bit vectors
8 years ago
dehnert
1f9e2967c8
some optimizations in explicit model building
8 years ago
dehnert
3a11914da0
commit to switch workplace
8 years ago
dehnert
c8e19d2e44
fixed priority queue implementation and upper reward bound computation
8 years ago
TimQu
1f2ab1a672
added function BitVector::fill() which sets all bits to true
8 years ago
TimQu
50e1fe0c15
increment() function for BitVector
8 years ago
TimQu
25074b50a9
Added function to get the next unset bit in a bitvector
8 years ago
Sebastian Junges
3a7ee7867b
rename files (does not compile)
9 years ago
dehnert
59a92a8941
support for labels in JANI models in sparse and dd engine
Former-commit-id: 34ad80be35
[formerly 67c09e4ff7
]
Former-commit-id: 1bf8ab71a1
9 years ago
dehnert
bba69684c9
reworked explicit Markov automaton generation a bit
Former-commit-id: 1ca8c9e828
[formerly 05ef68fdeb
]
Former-commit-id: c0f5830754
9 years ago
TimQu
f681206393
building markov automata from prism code
Former-commit-id: 791c49c7cf
9 years ago
Mavo
9d97750ca5
Improved compareAndSwap on BitVector
Former-commit-id: db953c187a
9 years ago
dehnert
fad28df7d6
first working version of next-state generator for PRISM models
Former-commit-id: 548a725e25
9 years ago
Mavo
f6374c60f8
Bitte ein Bit
Former-commit-id: ff11916b9a
9 years ago
dehnert
a75e0f5323
more work wrt cleaner model exploration
Former-commit-id: f24d618bdf
9 years ago
dehnert
33757633c8
first version of conditional probabilities for (non-parametric) DTMCs a la Baier
Former-commit-id: b57dfab024
10 years ago
sjunges
0cdca6a5fc
BitVector iterator +=
Former-commit-id: d9e02bce1a
10 years ago
sjunges
ebab145180
use default bitvector move, which is fine
Former-commit-id: e646a13fb5
10 years ago
sjunges
d4ba7905fa
Extra constructor for simple testing.
Former-commit-id: 0fcef3d5e7
10 years ago
sjunges
fd3ffafcd9
First version of the monolithic state space generation
Former-commit-id: fab8f6e356
10 years ago
dehnert
8868a50864
Removed superfluous code.
Former-commit-id: 06c2309d3c
10 years ago
dehnert
e1761fa774
Enabled hybrid CTMC model checker in cli. Further work on hybrid CTMC model checker (not yet working). Fixed some minor issues in sparse CTMC model checker.
Former-commit-id: f9c0f976e1
10 years ago
dehnert
a1dae8849e
Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented.
Former-commit-id: d4e6df30b5
10 years ago
dehnert
5e37c09fc0
Fixed some bugs.
Former-commit-id: dce463081d
11 years ago
dehnert
6f2916d557
Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet.
Former-commit-id: dc60f568bf
11 years ago
dehnert
26e9eac934
Added another convenience operation to bit vector class.
Former-commit-id: 6420f3ec90
11 years ago
dehnert
30f78b0a99
Intermediate commit. Started improving explicit model adapter performance.
Former-commit-id: 8a4aa64ac6
11 years ago
dehnert
53196f5610
Created bit vector hash map and some necessary bit vector methods.
Former-commit-id: 4a9946a743
11 years ago
dehnert
5bc593174e
Further work on weak bisimulation.
Former-commit-id: 3ad48ee0a3
11 years ago
dehnert
56aec18a48
Added bisimulation settings. Further work on weak bisimulation.
Former-commit-id: c04759575a
11 years ago
dehnert
d5cadc0f4b
Finalized interface of bit vector. Added unit tests for all methods of the bit vector.
Former-commit-id: 6c7834ed20
12 years ago
dehnert
30322ec57d
Now officially made the iterator over bit vectors an input iterator so that it can be used for constructing STL containers and other containers.
Former-commit-id: 1bcd8c43b3
12 years ago
dehnert
07fbff7a07
Started refactoring bit vector class.
Former-commit-id: a2fecfce2b
12 years ago
dehnert
344e1b6dd3
Enabled checking of some untimed properties on Markov automata.
Former-commit-id: e71aa66c62
12 years ago
dehnert
2cbdf56267
Fixed some bugs in bit vector and vector set that prevented the MEC decomposition from functioning correctly.
Former-commit-id: 51b6d7eb18
12 years ago
dehnert
5a9d778a23
First version of MEC decomposition for nondeterministic models.
Former-commit-id: 45f67b2a16
12 years ago
dehnert
b9130180ee
Rough sketch of MEC decomposition.
Former-commit-id: 027b58d380
12 years ago
dehnert
f287b7e760
Further steps towards implementation of MEC decomposition.
Former-commit-id: 8166b3b923
12 years ago
masawei
ee1c1eb9b6
First implementation of the BitVector to Dtmc subsystem converter in Dtmc.h
-Had to add a addState function to AtomicPropositionLabeling to be able to throw out the unneeded states using the substates constructor while at the end adding the absorbing state and its label.
An alternative for that would be to provide a constructor taking the mapping and the single labelings vector as well as a getter for the single labelings.
-The --counterexample command now only uses the pctl file given as argument to it and therefore it is now superflous to give the --prctl command in that case.
-Also fixed a bug in the filter constructor of the BitVector.
Now it copies all bit values specified by the filter to the correct index of new instance instead of all to index 0.
Next up: Handle the optionals of the Dtmc when creating the sub-Dtmc.
Former-commit-id: b45ee94cb2
12 years ago
dehnert
61e12601ed
Further step towards refactored ExplicitModelAdapter.
Former-commit-id: 8abc07a366
12 years ago
dehnert
f39fb24f65
Removed pointers from Model Checker Interface (and callback methods in formulas). From now on, the results are returned in form of an object. Because of the existing move semantics for the types in question, this does not come at a performance penalty.
Former-commit-id: 5befdebd92
12 years ago