sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
3610 Commits
2 Branches
0 Tags
187 MiB
Tree: 0c4b52cfa9
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '0c4b52cfa9'
${ noResults }
Commit Graph

67 Commits (0c4b52cfa9a937bc937e46dc53a8fcfcf4472b67)

Author SHA1 Message Date
dehnert 59a92a8941 support for labels in JANI models in sparse and dd engine
9 years ago
dehnert bba69684c9 reworked explicit Markov automaton generation a bit
9 years ago
TimQu f681206393 building markov automata from prism code
9 years ago
Mavo 9d97750ca5 Improved compareAndSwap on BitVector
9 years ago
dehnert fad28df7d6 first working version of next-state generator for PRISM models
9 years ago
Mavo f6374c60f8 Bitte ein Bit
9 years ago
dehnert a75e0f5323 more work wrt cleaner model exploration
9 years ago
dehnert 33757633c8 first version of conditional probabilities for (non-parametric) DTMCs a la Baier
9 years ago
sjunges 0cdca6a5fc BitVector iterator +=
10 years ago
sjunges ebab145180 use default bitvector move, which is fine
10 years ago
sjunges d4ba7905fa Extra constructor for simple testing.
10 years ago
sjunges fd3ffafcd9 First version of the monolithic state space generation
10 years ago
dehnert 8868a50864 Removed superfluous code.
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.
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.
10 years ago
dehnert 5e37c09fc0 Fixed some bugs.
10 years ago
dehnert 6f2916d557 Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet.
10 years ago
dehnert 26e9eac934 Added another convenience operation to bit vector class.
10 years ago
dehnert 30f78b0a99 Intermediate commit. Started improving explicit model adapter performance.
10 years ago
dehnert 53196f5610 Created bit vector hash map and some necessary bit vector methods.
10 years ago
dehnert 5bc593174e Further work on weak bisimulation.
11 years ago
dehnert 56aec18a48 Added bisimulation settings. Further work on weak bisimulation.
11 years ago
dehnert d5cadc0f4b Finalized interface of bit vector. Added unit tests for all methods of the bit vector.
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.
12 years ago
dehnert 07fbff7a07 Started refactoring bit vector class.
12 years ago
dehnert 344e1b6dd3 Enabled checking of some untimed properties on Markov automata.
12 years ago
dehnert 2cbdf56267 Fixed some bugs in bit vector and vector set that prevented the MEC decomposition from functioning correctly.
12 years ago
dehnert 5a9d778a23 First version of MEC decomposition for nondeterministic models.
12 years ago
dehnert b9130180ee Rough sketch of MEC decomposition.
12 years ago
dehnert f287b7e760 Further steps towards implementation of MEC decomposition.
12 years ago
masawei ee1c1eb9b6 First implementation of the BitVector to Dtmc subsystem converter in Dtmc.h
12 years ago
dehnert 61e12601ed Further step towards refactored ExplicitModelAdapter.
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.
12 years ago
PBerger 158430418e Replaced boost integer mask includes with cstdint
12 years ago
dehnert abf6f85b63 Intermediate commit to switch workplace.
12 years ago
PBerger bf5de84ab9 Refactored the parsing and lineFeeding handling.
12 years ago
PBerger 78184f9537 Added a Hash Class in the Utility Namespace.
12 years ago
dehnert f44f0ce410 Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility.
12 years ago
dehnert c8081c4d34 Fixed wrong step-bounded backward search.
12 years ago
dehnert 14fae4883a Added prob 0/1 precomputation for bounded-until model checking for DTMCs. The version for MDPs seems to perform worse: needs to be investigated.
12 years ago
Lanchid ec91dcbe2e Merge branch master into LTLParser
12 years ago
dehnert fc67cf4e3f Further refactoring of GraphAnalyzer class.
12 years ago
dehnert 94337f5835 Added move-constructor and move-assignment to bit vector class.
12 years ago
dehnert 102f38322d Fixed several bugs in several modules (bit vector, parser, etc.). Topological value iteration now works for the consensus protocol and the two dice example.
12 years ago
dehnert af1aa4e1e5 Added native matrix-vector multiplication for our matrix format (as fast as gmm++). Fixed bug in bit vector. Fixed some issues in SCC decomposition. MDP model checkers now have the solving methods by default (native ones) and may override them with their own ones, if desired. Added some aux stuff, like vector helper methods.
12 years ago
dehnert 34b85b956e Moved model checking of DTMCs to superclass. Now, each DTMC model checker only needs to implement matrix-vector multiplication and linear equation solving to be able to fully model check DTMCs. Added subset/disjoint functionality to bit vector. Changed tests for MDP and DTMC model checking a bit.
12 years ago
dehnert 4bcb26ab96 Included subset-test in bitvector.
12 years ago
Lanchid 5b57728d7e Merge branch master into PrctlParser
12 years ago
dehnert 7d7edc5a05 Implemented Prob1E algorithm for nondeterministic models. Added comparison operator to bit vector.
12 years ago
dehnert 7331544377 Added output functionality to bit vector and moved test-checking lines in storm.cpp to the right place.
12 years ago