b978a4d311
Added more move constructors.
Former-commit-id: 9770365fbb
12 years ago
89909fe8dc
Edited all Parsers to lose its class.
Modified many classes to provide a reference-constructor.
Fixed a few bugs in Tests.
Former-commit-id: c31fe95aae
12 years ago
f4050e5b18
Edited Parsers, re factored interface into a single function without an encapsulating class. Warning, this is work in Progress and not yet compiling.
12 years ago
e7601eb7b7
Included scheduler generation in model checking procedure for MDPs.
12 years ago
fabf662edd
Added dot output for both deterministic and nondeterministic models. Fixed iterator bug in sparse matrix.
12 years ago
4dadedf39d
Added methods to retrieve module index by variable name from IR. This fixes an issue in the symbolic adapter.
12 years ago
f44f0ce410
Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility.
12 years ago
1e5de29eec
Conversion adapter to create LTL2DStar formulas out of "ours"
12 years ago
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
a619303a1a
Removed unnecessary command line utilities.
12 years ago
ec91dcbe2e
Merge branch master into LTLParser
12 years ago
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
ed4c6c8429
Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer.
12 years ago
5f27a932a9
Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes.
12 years ago
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
a868980466
Fixed code so that tests compiles.
12 years ago
2e8d264594
Minor changes to state labeling class:
* marked some methods as const
* renamed getAtomicProposition to getLabeledStates
12 years ago
f899914799
Adapted the labeling class such that no raw arrays are included any more, but a vector instead.
12 years ago
3b76126f6b
Split PrismParser and PrismGrammar in differenc object files.
Added reset method for grammars, now we can parse multiple files in one program execution.
Added test for mdp parsing.
12 years ago
2b4d26023a
Fixed one of the remaining bugs introduced by refactoring.
12 years ago
00b4797948
Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.
12 years ago
9ae177c9b5
Further refactoring. In particular of the matrix class.
12 years ago
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
bdf173c315
GraphTransition objects can now be build from the SCC decomposition of a system.
12 years ago
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
df78cccf84
Fixed bug in graph transitions if initialization was done forward.
12 years ago
5e3a8a1232
Fixed wrong check for submatrix property of reward matrices.
12 years ago
7b259120b7
Marked submatrix check in DTMC and sparse matrix as faulty. Needs to be fixed.
12 years ago
5b57728d7e
Merge branch master into PrctlParser
12 years ago
0f9f5e67f6
A few minor fixes. Removed test for reward model.
12 years ago
d4cf812c5e
Added until-model checking for MDPs. Implemented Prob1A algorithm. Added asynchronous leader example.
12 years ago
7ceb1ed9b2
Added logging for errors in labeling class. Corrected wrong labeling of MDP in examples. Extended test checking for first MDP example in main.
12 years ago
8c248c05c5
Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm.
12 years ago
73ab4a78a9
Renamed methods get*Pointer in sparse matrix class, because they do not return a pointer. Added initial versions of forward/backward graph transition creation for nondeterministic models.
12 years ago
19cbe13691
Prepared methods for performing reachability searches for non-deterministic models. Removed storage of backward transition relation: it is now (re-)created on demand in the model checkers.
12 years ago
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
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
c02271a36a
Fixed typo in CTMC class. Moved GraphAnalyzer to utility.
12 years ago
afce8c9d12
Fixed some doxygen warnings
(Remaining warnings all appear because of undocumented function
parameters)
12 years ago
718608622f
added Ctmdp model, changed MdpParser to NonDetModelParser
12 years ago
54565ddd55
changed rowMapping to vector<int>
12 years ago
583ebf62bd
made rowMapping from NDSTParser available in MDP model class
12 years ago
1d1f9da315
made rowMapping from NDSTParser available in MDP model class
12 years ago
d23b3dbee5
First compiling version of PRCTL parser
12 years ago
4fd1d672ef
fixed valgrind errors
creating new shared_ptr instances from a raw pointer (i.e. shared_ptr<>(this) or alike) destroys the internal reference counting.
To make this work, one can use std::enable_shared_from_this(), which solves our problem here.
12 years ago
facec2b040
experimented with custom style checker, fixed a few minor issues
12 years ago
b13f1ff37f
Adding check "transitionRewards submatrix of transitions"
12 years ago
3dc82759af
some error output, if Dtmc matrix is invalid
12 years ago
7800132684
Added Mdp Class, Parser and support in the AutoParser.
Added Test for MdpParser
12 years ago
57274b3f09
Fixed missing newline and warning about nested comments.
12 years ago
PBerger
dehnert
Lanchid
gereon