81cf0e2b22
Added SparseMatrixBuilder class that actually builds the matrices. A call to build() will then generate the matrix. This eliminates superfluous checks in the matrix that slowed down performance.
Former-commit-id: af5d946fb8
12 years ago
97fb2f9750
All tests working with (partially) new sparse matrix implementation/interface.
Former-commit-id: 0272dd3524
12 years ago
a26f63be30
Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix.
Former-commit-id: 2c3b5a5bc3
12 years ago
84bd5f3b40
Renamed ConstTemplates to constants. Removed all calls to constGetZero, constGetOne and constGetInfinity by the new names. Created performance test for bit vector iteration.
Former-commit-id: 6d90ec961e
12 years ago
4550422fac
Added formula support for PRISM models. ExplicitModelAdapter now properly checks for out-of-bound values for integer variables.
Former-commit-id: 86439306b9
12 years ago
78d5f89ea2
Added formula support for PRISM models. ExplicitModelAdapter now properly checks for out-of-bound values for integer variables.
Former-commit-id: d990e1b388
12 years ago
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.
Former-commit-id: ac9993eab2
12 years ago
641c09dcfa
Fixed compile errors on windows caused by missing includes and use of initializer lists (not supported by vs11)
Former-commit-id: 294c26cd64
12 years ago
629448c312
First working version of MaxSAT-based minimal command counterexample generation.
Former-commit-id: 6dc49157f9
12 years ago
b6ff62e689
Towards adding more cuts to MaxSAT-based minimal command counterexamples. Some fixes here and there along the way.
Former-commit-id: 15ea8544fd
12 years ago
aec2596753
Several fixes for the IR. Weakest precondition computation is now supported for IR expressions.
Former-commit-id: 00387e59fc
12 years ago
f7a578e65d
Major change in PRISM grammars and IR: the IR now uses unique pointers instead of shared pointers to express ownership of objects more clearly.
Former-commit-id: 5b0228ee3b
12 years ago
121cbb7610
ExplicitModelAdapter now labels updates for synchronizing commands correctly.
Former-commit-id: ae9e6c9bda
12 years ago
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.
Former-commit-id: 105efc5342
12 years ago
84f1b192b4
Added globally unique indexes to updates in IR. Finalized support for labeled values in ExplicitModelAdapter. Modified tests to comply with the new usage of ExplicitModelAdapter.
Former-commit-id: f6d5a33d6d
12 years ago
61e12601ed
Further step towards refactored ExplicitModelAdapter.
Former-commit-id: 8abc07a366
12 years ago
a08a403eec
Ongoing refactoring work on ExplicitModelAdapter.
Former-commit-id: 1212f84aad
12 years ago
e2b0c4f1aa
Started refactoring ExplicitModelAdapter to finally make it nice.
Former-commit-id: 6df7e5d9fa
12 years ago
fdfb8ecc97
Minor fixes.
Former-commit-id: f2298d312a
12 years ago
84e7061a6d
Undefined constants are now undefined again after the explicit adapter has created the model (using specific constant values).
Former-commit-id: 96381b7d37
12 years ago
12a92fc6ee
Several fixes and additions to IR. Modifications to CMakeLists.txt of log4cplus to enable proper compilation under Mac OS. Fixes to coin2.nm. Added global variables to grammar and IR. Established basis for defining undefined constants of the model. Started to write MinimalLabelSetGenerator.
Former-commit-id: b65bb063fa
12 years ago
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.
Former-commit-id: 818431d6e9
12 years ago
0473d1a757
Fixed a lot of issues with the IR and the explicit state space generator.
Former-commit-id: fe80aaaf0f
12 years ago
01fd3c18e3
Added move constructors, added move-calls where fitting.
Former-commit-id: e73336c816
12 years ago
b978a4d311
Added more move constructors.
Former-commit-id: 9770365fbb
12 years ago
ec91dcbe2e
Merge branch master into LTLParser
12 years ago
cd9e2ba549
Some minor cleanups, added lot of documentation in prismparser
12 years ago
cb14f2e771
Made choiceIndices work in ExplicitModelAdapter, added code to somehow use --symbolic (parse model, show model information)
12 years ago
aafdbf7671
Fixed errors due to merging.
12 years ago
5495456991
Added new log level "trace"
Fixed bug in ExplicitModelAdapter
12 years ago
014ecd8597
Fixed some glitches, producing meaningful error if sum of probabilities for a command is not one
12 years ago
9613d099bb
Removed shared_ptr for module, program and rewardmodel objects.
12 years ago
1878962dea
Fixed another nullptr, removed shared_ptr for Update and Command objects.
12 years ago
152bcd2f20
Porting Program datastructures to use shared_ptr (at least for the moment...)
some more cleanups
12 years ago
5c25116a24
First version of ExplicitModelAdapter that supports transition rewards.
12 years ago
5f64fd168b
Cleaned up structure of ExplicitModelAdapter.
- added cpp file
- returns complete models now (missing transition rewards...)
12 years ago
5976c9e81d
More work for ExplicitModelAdapter
* Removed templates from various functions, as we can only produce double models anyway.
* Added methods to compute state rewards and state labelings
* Added toModel() routine
12 years ago
84993d24f8
Add documentation for ExplicitModelAdapter.
12 years ago
dfd601e126
fixed memory leak in addLabeledTransition and removed now obsolete functions.
12 years ago
52225ecf9c
Fixes to buildInitialStates.
12 years ago
772c03c070
Added routine to create all initial states.
Variables that have no explicit initial value will cause initial state for all possible values.
12 years ago
018e7ce056
some minor fixes.
Adapter now produces same result as prism for examples/dtmc/sync/sync.pm except order of nodes.
12 years ago
17d57e742a
Added code for labeled transitions.
New Adapter is basically finished, but not really tested ;-)
12 years ago
3464ef20c5
next chunk of code for new ExplicitModelAdapter.
now we have routines to create a result matrix from the intermediate representation, one for DTMCs and one for MDPs.
12 years ago
6d0d7e21c5
First chunk of code for new ExplicitModelAdapter.
The new adapter will generate an intermediate datastructure that holds all transitions to be inserted.
This will combine the two phases (computing the state space and actually generating the matrix) and can also be used for dtmc and mdp models.
This datastructure is only a list of maps for each state. Each map represents a nondeterministic choice and maps target node ids to their probability.
12 years ago
8f4f39d510
closed last memory leak...
12 years ago
34ca097eb3
fixed another more memory leak. One still missing...
12 years ago
58cf018371
Implemented synchronization in ExplicitModelChecker::buildMatrix().
This seems to produce the correct number of states and produces no valgrind errors. :-)
12 years ago
c33d319ac3
some minor fixes, now with less memory errors :)
12 years ago
de268ec3e8
Forgot to remove a *...
12 years ago
dehnert
David_Korzeniewski
PBerger
Lanchid
gereon