dehnert
59666a9fe9
slight renaming in matrix builder to better capture semantics
8 years ago
dehnert
99647c11fb
fixed an issue pointed out by Tim
8 years ago
dehnert
ac759d2671
minor performance improvements to model building
8 years ago
dehnert
6501fffac3
several optimizations related to explicit model building
8 years ago
sjunges
12dda40919
split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs
8 years ago
dehnert
3a11914da0
commit to switch workplace
8 years ago
dehnert
2d41de479e
added progress outputs to iterative solvers
8 years ago
dehnert
52b07a0c2f
fixed a bug in sparse matrix builder, fixed some tests
8 years ago
dehnert
29855e2853
added option to display information about exploration progress to both jit and explicit builder
8 years ago
TimQu
576f92568e
StateValuations and ChoiceOrigins are now members of a sparse::Model.
A model can now be constructed by providing a modelComponents struct.
8 years ago
TimQu
464bdc389c
improved state valuations class
8 years ago
TimQu
e7bc5fdef9
fixed several minor bugs regarding the choicelabeling
8 years ago
TimQu
759e351e95
Improved explicit model building:
- There is now an option to generate a choice labeling that corresponds to the specified action names.
- The old choice labeling (where each choice was labeled with an index set representing the corresponding prism commands) is renamed to choiceOrigins and has been improved towards support of other input formats (such as Jani) and other applications such as scheduler synthesis
8 years ago
Sebastian Junges
5894f7c706
some forward declarations and header updates to battle recompilation times
9 years ago
Sebastian Junges
d246517757
removed src prefix in all includes
9 years ago
Sebastian Junges
e1d201c85e
c++ code compiles again after rename
9 years ago
Sebastian Junges
3a7ee7867b
rename files (does not compile)
9 years ago
dehnert
4d8c765fdf
made jit-builder ready to deal with compositions that do not mention all automata, more work on rewards
Former-commit-id: 2faeed82fa
[formerly 60157bbec4
]
Former-commit-id: ea62a094f1
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
dehnert
ce5ca9d1ce
added proper action reward handling to JANI next-state generator
Former-commit-id: cd554d6e12
[formerly 47dfb5a796
]
Former-commit-id: 67a31637c5
9 years ago
Mavo
566cef0f91
Started on compiling without Carl
Former-commit-id: 5e0895d7c5
9 years ago
TimQu
12287e5090
small fix for building MAs
Also fixed a test for explicit MA parsing, where the transitions of a probabilistic choice did not sum up to one
Former-commit-id: c2f920a4d6
9 years ago
TimQu
f681206393
building markov automata from prism code
Former-commit-id: 791c49c7cf
9 years ago
dehnert
2a7dc0fad0
renamed MarkovChainSettings
Former-commit-id: 39024731f8
9 years ago
dehnert
f3fa90cc37
more work towards exact solving
Former-commit-id: 38edbcf2ca
9 years ago
dehnert
512a1ec558
added special label 'deadlock' to models and builders
Former-commit-id: 4edc57216e
9 years ago
dehnert
08112d98aa
more work on JANI next state generator and the corresponding tests
Former-commit-id: e170c9989c
9 years ago
dehnert
4cc780cbc0
tests compiling and running again
Former-commit-id: f84c73d0ae
9 years ago
dehnert
d35c99e844
renamed central model builder function
Former-commit-id: 92cfaeae19
9 years ago
dehnert
9f6bd1805f
modified the entry point code to deal with the new generator-builder-structure
Former-commit-id: f01a19e346
9 years ago
dehnert
ddf165d4d3
more work on tearing PRISM-specific functionality out of the explicit model builder
Former-commit-id: a835c9072e
9 years ago
dehnert
6655ee41d8
started to restructure explicit model builder to make it fit for JANI models
Former-commit-id: 69603dd97b
9 years ago
Mavo
a0d659f2da
always use shared_ptr<Formula const>
Former-commit-id: 63a447e887
9 years ago
dehnert
db3d1df863
added a sh*t ton of debug output, didn't help
Former-commit-id: a1bf88c024
9 years ago
dehnert
6d421a6fbe
learning seems to work find on first larger example
Former-commit-id: 706981a362
9 years ago
Mavo
c9f04ecc0b
Added IOSettings
Former-commit-id: 95946a7666
10 years ago
Mavo
effadc5cca
Split into general settings and markov chain settings
Former-commit-id: 619a2e3622
10 years ago
Mavo
67d77608bd
Refactoring of settings
Former-commit-id: ea4350fc1c
10 years ago
dehnert
fd615289e0
outline of learning algorithm
Former-commit-id: d770d1b7dc
10 years ago
dehnert
1fb943b658
moved some internal structs from model builder to their own files to make them reusable
Former-commit-id: a354059fe8
10 years ago
dehnert
ca354cffe4
moved preprocessing of PRISM program to utility to make it accessible from learning-based model checker
Former-commit-id: 704dde9ec5
10 years ago
dehnert
1f5439e270
added state labeling generator interface
Former-commit-id: eb7668741f
10 years ago
dehnert
ffe63ea95d
made dfs as exploration order available
Former-commit-id: 46ea31af78
10 years ago
dehnert
55fd1b66c3
introducing exploration orders to explicit builder
Former-commit-id: a56620eac2
10 years ago
dehnert
fff7b2d5db
fixed an allocation issue, performance is now roughly the same as before but memory consumption is reduced
Former-commit-id: ff44804975
10 years ago
dehnert
fad28df7d6
first working version of next-state generator for PRISM models
Former-commit-id: 548a725e25
10 years ago
dehnert
9eec5b140c
refactoring of model builder
Former-commit-id: f049f5a5bf
10 years ago
dehnert
a75e0f5323
more work wrt cleaner model exploration
Former-commit-id: f24d618bdf
10 years ago
dehnert
8a0bd32b55
tearing apart explicit model builder and 'next-state generation'
Former-commit-id: 2ccda8d931
10 years ago
dehnert
7ce969b312
started working on more flexible model generation using next-state-generators
Former-commit-id: 805940f179
10 years ago