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

11 Commits (1716c45ec549fd41f4e8e9d989547038fe8688e7)

Author SHA1 Message Date
masawei 1716c45ec5 Fixed compile errors concerning the handling of the STORM_HAVE_Z3 flag and a missing include in IRUtility.h
12 years ago
dehnert b6ff62e689 Towards adding more cuts to MaxSAT-based minimal command counterexamples. Some fixes here and there along the way.
12 years ago
dehnert d6c59e2ca3 Further work on MaxSAT-based minimal counterexample generator.
12 years ago
dehnert b860f16ada Further work on MaxSAT-based minimal command counterexamples.
12 years ago
dehnert aec2596753 Several fixes for the IR. Weakest precondition computation is now supported for IR expressions.
12 years ago
dehnert 20ae92e1ba Added support for cloning IR expressions.
12 years ago
dehnert 2cc5b6e080 Added Z3ExpressionAdapter to translate IR expressions to the Z3 format. Improvements to label-/command set generators. Disabled MILP-call from main().
12 years ago
dehnert bd3edb5f8b Naive enumeration of command set works.
12 years ago
dehnert a7dda9131b Intermediate commit to switch workplace.
12 years ago
dehnert e3234b54f3 Step towards minimal command generator using MaxSAT and model checking.
12 years ago
dehnert a45e9423b8 Sparse matrix can now also be used without knowing the number of rows/columns/nonzeros upfront. Adapted ExplicitModelAdapter to use that capability to not explore the state space twice. Added support for Z3 to CMakeLists.txt. Added correct submatrix checks for transition rewards in MDPs. Extended a test for the ExplicitModelAdapter a bit.
12 years ago