dehnert
|
05203792f2
|
fixed a couple of warnings
|
8 years ago |
dehnert
|
04d3a649bc
|
finalized location variable for JANI automata
|
8 years ago |
dehnert
|
d6a32ca634
|
more work on flattening JANI compositions
|
8 years ago |
dehnert
|
137aa163f2
|
fixed jit builder to not ignore locations
|
8 years ago |
Sebastian Junges
|
d246517757
|
removed src prefix in all includes
|
8 years ago |
Sebastian Junges
|
e1d201c85e
|
c++ code compiles again after rename
|
8 years ago |
Sebastian Junges
|
3a7ee7867b
|
rename files (does not compile)
|
8 years ago |
dehnert
|
e799cbba79
|
Updated exprtk. made exprtk case-sensitive. fixed other minor issues
Former-commit-id: 3557c83ab6 [formerly 747702a205 ]
Former-commit-id: 64a2265311
|
8 years ago |
dehnert
|
ae8a963c33
|
added some debug output to JaniNextStateGenerator
Former-commit-id: 2c116cf22b [formerly 98c11d0ce2 ]
Former-commit-id: bc3a09342a
|
8 years ago |
dehnert
|
b579978938
|
cleaned up jit model builder, added options, added doctor procedure, prepared Markov automata
Former-commit-id: bb8d1d95cc [formerly 6deb9e19a0 ]
Former-commit-id: d6b8563723
|
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
|
ad96b81a8a
|
fix to compile again
Former-commit-id: c0400b2dd3 [formerly 18685c4259 ]
Former-commit-id: 4806097817
|
9 years ago |
dehnert
|
44c06641d7
|
slightly different approach to transient variable handling
Former-commit-id: ed55cea083 [formerly 24237d79cf ]
Former-commit-id: 73157b53cc
|
9 years ago |
dehnert
|
2471036df4
|
more work on jit-thing: transitioning to proper handling of synchronizing edges
Former-commit-id: 3af1772192 [formerly 890c529dd1 ]
Former-commit-id: 818295a085
|
9 years ago |
dehnert
|
00db8794e6
|
fixed bug in explicit jani model generator
Former-commit-id: 445ee6a4ba [formerly 702d0fb0de ]
Former-commit-id: 0fb52d40d4
|
9 years ago |
dehnert
|
91e6bb2999
|
fixed bug in DD-based JANI model generation related to transient edge assignments
Former-commit-id: b2cf168189 [formerly 0c50ca2d16 ]
Former-commit-id: 05686fd6f1
|
9 years ago |
dehnert
|
011e3fbaa6
|
fixed bug that introduced transient variables in the state space
Former-commit-id: b335cf0c0d [formerly 84339f7943 ]
Former-commit-id: 6f64020873
|
9 years ago |
dehnert
|
59a92a8941
|
support for labels in JANI models in sparse and dd engine
Former-commit-id: 34ad80be35 [formerly 67c09e4ff7 ]
Former-commit-id: 1bf8ab71a1
|
9 years ago |
dehnert
|
269041feda
|
implemented lifting edge-destination assignments to edges as a JANI preprocessing step
Former-commit-id: 2aea0d3eb7 [formerly 6e16d3336d ]
Former-commit-id: 04843c9749
|
9 years ago |
dehnert
|
f49a2cf5a9
|
added proper location handling to JANI next-state generator
Former-commit-id: bd06465daa [formerly 5a5c6f7629 ]
Former-commit-id: 05a2e55d20
|
9 years ago |
dehnert
|
d3cf9a4e7f
|
adding Markov automaton tests to explicit JANI model builder
Former-commit-id: 634fe9c08e [formerly 73bbe89f78 ]
Former-commit-id: bb9339a947
|
9 years ago |
dehnert
|
c9c5f562a5
|
removed rename composition, because it is just a special case of synchronization vectors
Former-commit-id: 64d8c56019 [formerly 321c76e347 ]
Former-commit-id: 81d5237064
|
9 years ago |
dehnert
|
675b7bb207
|
added proper check for undefined constants when building explicit JANI models in non-parametric mode
Former-commit-id: 95c0bfc003 [formerly 3708bf3b69 ]
Former-commit-id: e5bbd290f3
|
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 |
sjunges
|
79c9dbcfda
|
OrderedAssignments
Former-commit-id: 91a9125db1 [formerly 69a5020cf6 ]
Former-commit-id: 33cc0a7137
|
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 |
dehnert
|
99badd02c5
|
more work towards JANI reward models
Former-commit-id: 4be9f840c4 [formerly be67354311 ]
Former-commit-id: b8ea6172e7
|
9 years ago |
dehnert
|
2a7e4a3c55
|
towards DD-based JANI rewards
Former-commit-id: 36d6cfbca3 [formerly c9d5074292 ]
Former-commit-id: b8fe7376b3
|
9 years ago |
dehnert
|
8a8aca0062
|
explicit reward model building for JANI working from cli
Former-commit-id: 22b4dbcdbf [formerly 4edbdf4207 ]
Former-commit-id: e93b8bf1a0
|
9 years ago |
dehnert
|
23809f54f1
|
first version of rewards for JANI models (explicit next-state generator only)
Former-commit-id: b2b0638427 [formerly c763581e06 ]
Former-commit-id: a032da1cff
|
9 years ago |
dehnert
|
2182beefcb
|
created storage class for JANI assignments that guarantees ordering
Former-commit-id: 6cc43016a2 [formerly aaa7b8a213 ]
Former-commit-id: 8eb1c8d54d
|
9 years ago |
dehnert
|
eed0a98899
|
commit to switch workplace
Former-commit-id: da2d6f8af3 [formerly f2157cac64 ]
Former-commit-id: 1b7b4b6496
|
9 years ago |
dehnert
|
7af89f5a6f
|
real transient variables and assignments are now added in PRISM to JANI transformation
Former-commit-id: 45ccd46071 [formerly a8d1de9c6a ]
Former-commit-id: 6aa6dbae52
|
9 years ago |
dehnert
|
e6d9c85749
|
fixed some bugs related to simplifaction of PRISM programs
Former-commit-id: 3c81bcac8d
|
9 years ago |
Mavo
|
566cef0f91
|
Started on compiling without Carl
Former-commit-id: 5e0895d7c5
|
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
|
71bfb45220
|
added check for multiple writes to the same global variable in explicit JANI next-state generator
Former-commit-id: 5fc1bb01a9
|
9 years ago |
dehnert
|
7861df4f20
|
JANI next-state generator appears to be working (without rewards)
Former-commit-id: 3ca5c3ccf2
|
9 years ago |
dehnert
|
08112d98aa
|
more work on JANI next state generator and the corresponding tests
Former-commit-id: e170c9989c
|
9 years ago |
dehnert
|
05fecb03b3
|
started on introducing multiple initial locations in JANI models
Former-commit-id: cf009b3e14
|
9 years ago |
dehnert
|
b62f8819b9
|
JANI next-state generator can now generate transitions from silent edges
Former-commit-id: 57e37b5850
|
9 years ago |
dehnert
|
000a8c2d77
|
more work on JANI next-state generator
Former-commit-id: d94ab2b81e
|
9 years ago |
dehnert
|
1d3539ab9a
|
factored out some parts from the PRISM next-state generator into the superclass
Former-commit-id: bb40e2ec4b
|
9 years ago |