1edbac40de
Clean up
7 years ago
d781584dfb
accumulation: support simple trafo
7 years ago
0fd6f9ac5c
Begin support for simple accumulation trafo
7 years ago
1616ded046
Clean up AccumulationTransformation
7 years ago
1b6e9e5ac6
Parser refresh
7 years ago
20712738e2
Clean up
7 years ago
c2ceb299dd
accumulation: add track status to Product.toDot
7 years ago
99d91a5f9d
accumulation: fix behaviour for step 0
7 years ago
fe968fb469
Parser refresh
7 years ago
b707e2def3
accumulation: Enable parsing of U+ Formulas
7 years ago
7cba802977
parser refresh
7 years ago
e6de4fc3f9
accumulation: rewrite engine
This rewrite changes the formula tranlation to use the pattern
init ^ run U goal
This allows to use the U+ operator and enables stuttering.
Note: U+ cannot be parsed yet.
7 years ago
a8e412c4a1
accumulation: deduplicate gensym
7 years ago
3f1474c32c
accumulation: fix up rebase
7 years ago
2ab6add12f
accumulation: fail on wrong engine
7 years ago
9e8a43f670
accumulation: print dotfile for DFA product
9 years ago
d3ba0c5d29
automata.finite: deduplicate toDot()
9 years ago
a540f87788
accumulation: documentation and refactoring
9 years ago
385884a590
accumulation: further refactoring of Product
9 years ago
327952ab52
accumulation: some fixes
* use Dottable interface
* rewrite the way tracks and their goodness are updated
9 years ago
43a5a91872
accumulation: don't try to print the model all the time...
9 years ago
8767e034ee
accumulation: add option accgeneratedots to generate DOT files
9 years ago
00d9bd162f
accumulation: don't advance good tracks
9 years ago
90511afb27
accumulation: refactor some common function in product
9 years ago
6740da5171
accumulation: some fixes
- length of longest path vs number of tracks
- typed accumulation states
9 years ago
ea87b6ec79
accumulation: fix product dot output
9 years ago
99bb5899c1
accumulation: snapshot from accumulation-mixed
9 years ago
6edb99dae9
automata.finite: use Dottable
9 years ago
62d9bacd94
common: interface for DOT-file generation
9 years ago
51f71b2b7a
automata.finite: remove some imports
9 years ago
2ea82a99a2
automata.finite: toDot methods for DFA
9 years ago
4dac6f64c1
Bugfixes for NFA/DFA-Library
* Reversing NFA: Fixed Iterating issue
* Determinisation: Fixed issue for initial and accepting state in DFA
* Determinisation: Take over APs
* Adding complete-Function for DFAs
* Other minor bugfixes
* Adding minor helper functions
9 years ago
95f7208c05
automata/finite: initial version
9 years ago
95a5f843f6
imported patch ProbModel-comments-for-constructor.patch
7 years ago
9f3f8bc820
imported patch explicit-MDP-prob01ae-with-prerel-compute-strat.patch
7 years ago
4d42482618
imported patch explicit-mdp-prob01-rel.patch
7 years ago
37a8adbe41
(TODO) IncomingChoiceRelation: calculatePreStar
TODO: optimize data types (Stack, BitSets)?
7 years ago
28dd4cd3eb
imported patch ChoicesMask.patch
7 years ago
ffc2cf9723
imported patch BitSetTools-prelim.patch
7 years ago
ae22faf097
imported patch MultiObjective-support-lowerbounds-via-LTL.patch
7 years ago
c70db33e06
imported patch activate-ltl-step-bounds.patch
7 years ago
0038984be4
imported patch ExpandStepBoundsSyntactically.patch
7 years ago
0ed7e6cec6
imported patch time-bounded-not-supported-message.patch
7 years ago
881ecfef2f
imported patch predecessor-LTLMC-use-backward.patch
7 years ago
e03cf7dbe5
imported patch predecessor-ec-computer-use-backward.patch
7 years ago
c17d91c1e6
imported patch predecessor-ECComputer.setPre.patch
7 years ago
19d8e743eb
imported patch predecessor-restrict-diagnostics.patch
7 years ago
da4eda6c5d
imported patch NondetModelChecker-cosafety-guard-against-rewards.patch
7 years ago
59a8c994d1
imported patch Wrapper.patch
7 years ago
51b0319520
imported patch symb-counter-transform-ProbModelChecker-protect-dtmc-trew.patch
7 years ago
Sascha Wunderlich