sjunges
|
98a1a531c2
|
Silent actions fixed; probability exported correctly.
Former-commit-id: 20ef70c4b3 [formerly 7a4d7ee1d8 ]
Former-commit-id: 44f344d2a2
|
8 years ago |
sjunges
|
deaaa91c37
|
Expressions & Destinations Assignments
Former-commit-id: dacc1f7146 [formerly 1580bce6a4 ]
Former-commit-id: a089bbd11a
|
8 years ago |
sjunges
|
79c9dbcfda
|
OrderedAssignments
Former-commit-id: 91a9125db1 [formerly 69a5020cf6 ]
Former-commit-id: 33cc0a7137
|
8 years ago |
sjunges
|
c8f2fc1df1
|
Added location names to destinations, added action names to edges, added types to constants
Former-commit-id: f974dc34cd [formerly 49717e521c ]
Former-commit-id: 669eef887f
|
8 years ago |
sjunges
|
a1e13b4c0a
|
First version of JSON exporter, export is not ocmplete (destination assignments, edge assignments, edge action names, destination locations, expressions(!), sync are missing)
Former-commit-id: 4c816ef4b2 [formerly 79fe84a8bb ]
Former-commit-id: b841b31f7a
|
8 years ago |
sjunges
|
20eaac6918
|
Convenience function in model and automaton, building explicit mappings (independent of implementation)
Former-commit-id: e183ae7ea8 [formerly 62b52cb78b ]
Former-commit-id: 8204f5b655
|
8 years ago |
sjunges
|
1557983f8b
|
Jani Export settings and code
Former-commit-id: ccd9955a99 [formerly 64edf38f14 ]
Former-commit-id: 0d3de2ad09
|
8 years ago |
sjunges
|
cd338eb8e3
|
hasMultipleLevel for orderedassignments
Former-commit-id: d1a94d6931 [formerly e19b59fdac ]
Former-commit-id: 9c79f94cdf
|
8 years ago |
sjunges
|
a7ff22bd49
|
Added to_string for ModelType
Former-commit-id: e1cf746727 [formerly 912ca0f4f3 ]
Former-commit-id: 9ebb580890
|
8 years ago |
dehnert
|
f616bf606b
|
adapted JANI parallel composition class to synchronization vector usage
Former-commit-id: 71322c70f0 [formerly ec71a5adc5 ]
Former-commit-id: ccdb40b1f3
|
8 years ago |
sjunges
|
5eac1e22ce
|
Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support
Former-commit-id: c8e7079004 [formerly d9b79118bf ]
Former-commit-id: 749e0dca53
|
8 years ago |
sjunges
|
b2ca743422
|
ProgramGraph->Jani (only locations & variables)
Former-commit-id: 70324d2df4 [formerly e17bc3cffd ]
Former-commit-id: bafb2e72ad
|
8 years ago |
sjunges
|
6f0a26e593
|
JaniExportSettings
Former-commit-id: d375a92788 [formerly 9bd2c0efa8 ]
Former-commit-id: f4e93f61dd
|
8 years ago |
sjunges
|
6f12a81505
|
program graph
Former-commit-id: 34b6394d24 [formerly 99be317a04 ]
Former-commit-id: 0c78bdf77e
|
8 years ago |
sjunges
|
8f8ef1564b
|
Builder for ProgramGraphs, for now, ignores actions.
Former-commit-id: 5f51f17e17 [formerly 1e48ddd098 ]
Former-commit-id: 80434a7402
|
8 years ago |
sjunges
|
5485abe1ef
|
Added pgcl to jani option in the settings
Former-commit-id: df76e91322 [formerly 334d45e88c ]
Former-commit-id: eede3e3d43
|
8 years ago |
dehnert
|
24e89ecce6
|
properly scaling state-action rewards for DTMCs in JANI model now
Former-commit-id: a70c5c3c6e [formerly 8d2a346735 ]
Former-commit-id: cad11b1b3f
|
8 years ago |
dehnert
|
ce5ca9d1ce
|
added proper action reward handling to JANI next-state generator
Former-commit-id: cd554d6e12 [formerly 47dfb5a796 ]
Former-commit-id: 67a31637c5
|
8 years ago |
sjunges
|
2356e4a7af
|
Good old const correctness added to all pgcl structs.
Former-commit-id: 387e3f7206 [formerly 5d53a2e8d3 ]
Former-commit-id: d4a7f36efd
|
8 years ago |
dehnert
|
99badd02c5
|
more work towards JANI reward models
Former-commit-id: 4be9f840c4 [formerly be67354311 ]
Former-commit-id: b8ea6172e7
|
8 years ago |
sjunges
|
c527646ddb
|
Added convenience operator overloads for more readable code :)
Former-commit-id: 082f19bede [formerly 94b4f6284f ]
Former-commit-id: c95b0dc93f
|
8 years ago |
sjunges
|
7d5d14f9b5
|
Removed flag nrVariables which was never updated
Former-commit-id: 7955de2fe8 [formerly 4015219cea ]
Former-commit-id: 7e5f23f84b
|
8 years ago |
dehnert
|
2a7e4a3c55
|
towards DD-based JANI rewards
Former-commit-id: 36d6cfbca3 [formerly c9d5074292 ]
Former-commit-id: b8fe7376b3
|
8 years ago |
dehnert
|
c2cab571f5
|
made tests work again
Former-commit-id: bd3e831b0d [formerly cef4348674 ]
Former-commit-id: 8fd0b70c1e
|
8 years ago |
dehnert
|
8a8aca0062
|
explicit reward model building for JANI working from cli
Former-commit-id: 22b4dbcdbf [formerly 4edbdf4207 ]
Former-commit-id: e93b8bf1a0
|
8 years ago |
dehnert
|
e274cd33eb
|
adapted cli to use symbolic model description rather than PRISM program
Former-commit-id: d06884a848 [formerly 9a128e04f1 ]
Former-commit-id: 25a820d000
|
8 years ago |
dehnert
|
d5ba9e00e8
|
started on making jani available from cli, commit to switch workplace
Former-commit-id: 4c04d77409 [formerly 279141117d ]
Former-commit-id: e05805177e
|
8 years ago |
dehnert
|
7c9c55b09c
|
added 'superclass' for PRISM program and JANI model so they can be handled as symbolic model descriptions
Former-commit-id: 748069c151 [formerly 2c3e462958 ]
Former-commit-id: e8d3ceb693
|
8 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
|
8 years ago |
sjunges
|
82ed6447f8
|
Parser changes for last commit.
Former-commit-id: 98b359de79 [formerly ae2143b72b ]
Former-commit-id: 9a61ed679b
|
8 years ago |
sjunges
|
359b62868c
|
Pgcl: Refactorign and introduced blocks
Former-commit-id: 9c493a8d6c [formerly 5ac9dc524e ]
Former-commit-id: 1931feb6ab
|
8 years ago |
dehnert
|
2182beefcb
|
created storage class for JANI assignments that guarantees ordering
Former-commit-id: 6cc43016a2 [formerly aaa7b8a213 ]
Former-commit-id: 8eb1c8d54d
|
8 years ago |
dehnert
|
eed0a98899
|
commit to switch workplace
Former-commit-id: da2d6f8af3 [formerly f2157cac64 ]
Former-commit-id: 1b7b4b6496
|
8 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
|
8 years ago |
dehnert
|
c0d1628466
|
made Prism to JANI conversion compile again
Former-commit-id: 7775fd4a18 [formerly f7a542bf3e ]
Former-commit-id: 0c0f7cf70b
|
8 years ago |
dehnert
|
9a5d11a5e0
|
adding real variables to JANI models. started to encapsulate PRISM to JANI converter
Former-commit-id: a7892b3d23 [formerly 411e830ca5 ]
Former-commit-id: 49ee703493
|
8 years ago |
dehnert
|
3d426798b3
|
added visitor that checks for syntatical equality of expressions
Former-commit-id: b6753a4891 [formerly 2b36b42bfa ]
Former-commit-id: f693de5f30
|
8 years ago |
dehnert
|
71f99eb075
|
Merge remote-tracking branch 'origin/future' into jani_support
Former-commit-id: 2c2c57e103 [formerly 8d725b4d90 ]
Former-commit-id: 918275a8c7
|
8 years ago |
dehnert
|
92932fced1
|
support for initial constructs in PRISM programs
Former-commit-id: 0c8132aa43
|
8 years ago |
sjunges
|
0f6a741276
|
pgcl
Former-commit-id: 63d52fc706 [formerly 90b7939792 ]
Former-commit-id: 04e29e8c41
|
8 years ago |
dehnert
|
12ac3549da
|
adapted relevant parts to new way of specifying initial values/restrictions
Former-commit-id: a55abbe3b6 [formerly 6a9d8a6a55 ]
Former-commit-id: 47799adaf2
|
8 years ago |
dehnert
|
b405a67b54
|
removed RewardIncrement. fixed PRISM to JANI converter
Former-commit-id: c189fa8e60 [formerly 63dccbdb95 ]
Former-commit-id: 36449defd0
|
8 years ago |
dehnert
|
1b19372a14
|
changed a default argument initializer list to make compilers happier
Former-commit-id: 41dcbd2f10
|
8 years ago |
TimQu
|
d1ea675245
|
Added missing case for Power when converting to z3::expr
Former-commit-id: 4279fba636
|
8 years ago |
dehnert
|
a8383a283d
|
fixed wrong header inclusion in previous commit
Former-commit-id: f91e63cccd
|
8 years ago |
dehnert
|
96891acfe7
|
included missing (at least for some compilers) header
Former-commit-id: 4792acf519
|
8 years ago |
ThomasH
|
b930ed0dde
|
use int instead of string ids
Former-commit-id: 91c6eda5c6
|
8 years ago |
dehnert
|
bcb13a4fe1
|
moved deletion of commands (if guard becomes false) from Program::substitute to Program::simplify
Former-commit-id: ec5b4d4a57
|
8 years ago |
dehnert
|
3ea11188b7
|
fixed an issue in the CMakeLists.txt that prevented carl from being properly loaded if it's not already present
Former-commit-id: 95b83d3988
|
8 years ago |
dehnert
|
e6d9c85749
|
fixed some bugs related to simplifaction of PRISM programs
Former-commit-id: 3c81bcac8d
|
8 years ago |