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

33 Commits (6eb846da9714dc63a8142cc266c046a52362c32f)

Author SHA1 Message Date
dehnert db232fe39b Moved from pair to MatrixEntry as the basic building block of the matrix. Now matrix elements can be accessed in a more readable way.
11 years ago
dehnert 12743e0a7e Moved from additional row grouping to the one embedded in the matrix itself.
11 years ago
dehnert 38833e308f Started to add row-grouping to sparse matrix class.
11 years ago
dehnert 35d16a1191 Replaced VectorSet bei boost::container::flat_set, which does essentially the same. Fixed a bug in sparse matrix creation.
11 years ago
dehnert f684ce7799 Removed obsolete constructors of sparse matrix class as the new matrix builder is supposed to be used anyway. Fixed some minor issues.
11 years ago
dehnert cf2b84b281 Further work on iterators for sparse matrix.
11 years ago
dehnert a26f63be30 Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix.
11 years ago
dehnert 2cbdf56267 Fixed some bugs in bit vector and vector set that prevented the MEC decomposition from functioning correctly.
11 years ago
masawei 84f6bf7104 Added a getBackwardsTransitions() to AbstractNondeterministicModel, since simple transposition does not yield correct results and for the computation of the backwards transitions the nondeterministic choice indices must be known.
11 years ago
dehnert 9e941e6b4a Added scheduler classes. Added method to model classes that applies a scheduler.
11 years ago
dehnert 422da8f481 Added set class with an underlying vector container. Adapted code in counterexample generators to use the new set class. Still bugs in it though.
11 years ago
dehnert a45e9423b8 Sparse matrix can now also be used without knowing the number of rows/columns/nonzeros upfront. Adapted ExplicitModelAdapter to use that capability to not explore the state space twice. Added support for Z3 to CMakeLists.txt. Added correct submatrix checks for transition rewards in MDPs. Extended a test for the ExplicitModelAdapter a bit.
11 years ago
dehnert 61e12601ed Further step towards refactored ExplicitModelAdapter.
11 years ago
PBerger e0ee4ea2fd Implemented a method for generating a choiceLabeling based on the stateIds
11 years ago
dehnert 816f12f2f6 Added global variables to string output of probabilistic program. Added number of choices to model information output of nondeterministic models.
11 years ago
dehnert 947581dd25 Refactored and fixed bugs in explicit model adapter. Added support for labeling of choices of a model. The explicit model adapter uses that functionality to label each choice with the involved PRISM commands.
11 years ago
dehnert 15542d46da Changes:
12 years ago
dehnert 5776b207c3 Changed to new cleaner iterator for matrix.
12 years ago
dehnert 36543de851 Started trying to implement a more clean iterator solution for sparse matrix.
12 years ago
dehnert 41db9a8092 Small changes to MDP model checker.
12 years ago
PBerger 01fd3c18e3 Added move constructors, added move-calls where fitting.
12 years ago
PBerger 4212858013 Fixed a few Rebasing Issues.
12 years ago
PBerger 484c4e8151 Added more debugging output into the MDP Model
12 years ago
PBerger fb3209dfc3 Added missing template parameters in the abstract models
12 years ago
PBerger 78184f9537 Added a Hash Class in the Utility Namespace.
12 years ago
PBerger b978a4d311 Added more move constructors.
12 years ago
PBerger 89909fe8dc Edited all Parsers to lose its class.
12 years ago
dehnert e7601eb7b7 Included scheduler generation in model checking procedure for MDPs.
12 years ago
dehnert fabf662edd Added dot output for both deterministic and nondeterministic models. Fixed iterator bug in sparse matrix.
12 years ago
dehnert f44f0ce410 Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility.
12 years ago
Lanchid ec91dcbe2e Merge branch master into LTLParser
12 years ago
dehnert fbe1f41213 Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests.
12 years ago
dehnert ed4c6c8429 Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer.
12 years ago
dehnert 5f27a932a9 Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes.
12 years ago
dehnert 69395face2 Moved creation of SCC-dependency graph into abstract model class. Added functionality to sparse matrix class to not give the number of nonzeros upfront, but to to grow on demand.
12 years ago
gereon a868980466 Fixed code so that tests compiles.
12 years ago
Lanchid 5b57728d7e Merge branch master into PrctlParser
12 years ago
dehnert 8c248c05c5 Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm.
12 years ago
dehnert 84c159feba Moved model information output to super class. Moved methods to determine data structure size to superclass(es). Added missing getType methods for some models.
12 years ago
dehnert 7d95a45633 Fixed bug in AbstractModelChecker: it does now correctly inherit from a lot more interface classes. NOTE: checking a formula on a model checker that does not support it failed silently. This should NOT be the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled anyway? Introduced another layer AbstractDeterministicModel and AbstractNonDeterministicModel in model hierarchy to allow for easily distinguishing these classes. Made necessary adaptions in (hopefully) all classes. Move the graph analyzer to utility folder.
12 years ago