sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
5098 Commits
2 Branches
0 Tags
187 MiB
Tree: 6a2f810ccc
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '6a2f810ccc'
${ noResults }
Commit Graph

5098 Commits (6a2f810ccc33578b68b9d8e69c3444801bc858cd)
 

Author SHA1 Message Date
dehnert e274cd33eb adapted cli to use symbolic model description rather than PRISM program
9 years ago
dehnert d5ba9e00e8 started on making jani available from cli, commit to switch workplace
9 years ago
dehnert 7c9c55b09c added 'superclass' for PRISM program and JANI model so they can be handled as symbolic model descriptions
9 years ago
dehnert 23809f54f1 first version of rewards for JANI models (explicit next-state generator only)
9 years ago
sjunges 82ed6447f8 Parser changes for last commit.
9 years ago
sjunges 359b62868c Pgcl: Refactorign and introduced blocks
9 years ago
dehnert 2182beefcb created storage class for JANI assignments that guarantees ordering
9 years ago
dehnert eed0a98899 commit to switch workplace
9 years ago
dehnert 7af89f5a6f real transient variables and assignments are now added in PRISM to JANI transformation
9 years ago
dehnert c0d1628466 made Prism to JANI conversion compile again
9 years ago
dehnert 9a5d11a5e0 adding real variables to JANI models. started to encapsulate PRISM to JANI converter
9 years ago
dehnert 3d426798b3 added visitor that checks for syntatical equality of expressions
9 years ago
dehnert 71f99eb075 Merge remote-tracking branch 'origin/future' into jani_support
9 years ago
dehnert 92932fced1 support for initial constructs in PRISM programs
9 years ago
sjunges 0f6a741276 pgcl
9 years ago
dehnert 12ac3549da adapted relevant parts to new way of specifying initial values/restrictions
9 years ago
dehnert b405a67b54 removed RewardIncrement. fixed PRISM to JANI converter
9 years ago
dehnert ae0e423a4e Merge remote-tracking branch 'origin/future' into menu_games
9 years ago
dehnert 1b19372a14 changed a default argument initializer list to make compilers happier
9 years ago
TimQu b362047e4f mutex example
9 years ago
dehnert 059f55eefc commit to switch workplace, debugging in progress
9 years ago
dehnert 673c329311 prepared upcoming fix for refinement based on quantitative information
9 years ago
dehnert 7100dfa3a7 Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games
9 years ago
dehnert 156ab071a5 more work on abstraction refinement
9 years ago
PBerger d76e9729da Leave Replacement finally working.
9 years ago
dehnert 4431df82a0 Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games
9 years ago
dehnert bc1eff959f graph algorithms for games now also compute player 2 prob0/1 states and the generated strategies are adapted accordingly
9 years ago
PBerger c9f2eef826 Added functionality for replacing leaves in SRF MTBDDs.
9 years ago
TimQu ee59f772b0 fixed prism code for polling example
9 years ago
TimQu 6291527576 Merge branch 'future' into multi-objective
9 years ago
TimQu d1ea675245 Added missing case for Power when converting to z3::expr
9 years ago
TimQu e1aca37c86 some minor tweaks plus polling example
9 years ago
TimQu 3897f9c417 Merge remote-tracking branch 'origin/future' into multi-objective
9 years ago
dehnert d16e47882d fixed bug and added tons of debug output
9 years ago
TimQu ee8d345667 csl MA model checker does not allow rational numbers
9 years ago
PBerger d3c492124a Fixed min/max Abstract w. repr.
9 years ago
dehnert a663a37e21 fixed a bug that prevented correct strategy generation in iterative solver
9 years ago
dehnert 20f07bf291 added incremental strategy generation to symbolic game solver and removed some debug output
10 years ago
dehnert a0ad4b25de corrected minor typo
10 years ago
dehnert 375ea1b194 fixed bug in cudd minAbstractRepresentative, adapted tests, passing now
10 years ago
dehnert 39de9561cd Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games
10 years ago
dehnert f45b7f9171 fixed some bugs and started on quantitative refinement
10 years ago
PBerger da199866e6 Added tests for minAbstractRepresentative.
10 years ago
dehnert 66b0817a35 fixed bugs here and there
10 years ago
dehnert 142eb96736 hopefully fixing cudd's min/maxAbstractRepresentative
10 years ago
dehnert 42af59ef5d Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games
10 years ago
PBerger 68b14b3076 Moved BDD functionality in Sylvan to sylvan_bdd_int.h to allow reuse.
10 years ago
dehnert 56b5b98a2c towards strategy generation in game solver
10 years ago
dehnert bde84d0073 fixed symbolic game solver wrt. illegal masks. numerical solving step in game-based model checker working, but no refinement yet.
10 years ago
dehnert 8b29ab079c fixed some bugs in custom cudd functions
10 years ago