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

107 Commits (86f5cda3d407b139c591567e8b13d0e47cf78135)

Author SHA1 Message Date
Tim Quatmann 324eb23cdd Using new LRA environment
7 years ago
Tim Quatmann 8a23197a77 Fix for LRA scheduler generation.
7 years ago
Tim Quatmann 009cee1c25 Implemented scheduler extraction for LRA properties for MDP.
7 years ago
Tim Quatmann c1b3a4f991 LraMdpPrctlModelCheckerTest: Test LRA computation for different environments. Added a testcase.
7 years ago
Matthias Volk 6a4c18e4a2 Use custom FlatSet to account for allocator changes in flat_set in Boost 1.70.
7 years ago
Tim Quatmann bc623d1203 MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler.
8 years ago
Tim Quatmann bce641319f Fixed computation of maximal total expected rewards for MDPs with end components.
8 years ago
TimQu dd93b1dae9 rewardbounded: Improved code structure.
8 years ago
Tim Quatmann 82402ba3ae rewardbounded: Moved epoch model analysis to a separate file.
8 years ago
TimQu c614e9d747 Fixed Value Iteration based LRA computation
8 years ago
TimQu 985319c7dd Tweaked LRA computation for MDPs and MAs in sound mode to meet precision requirements.
8 years ago
Sebastian Junges 43688d09ea reward infinity scheduler extraction is now correct
8 years ago
Sebastian Junges 93ca559c83 additional sanity checks for scheduler extraction
8 years ago
Sebastian Junges 16d7dccb4e I am utterly stupid. Fixed an assertion that I changed yesterday
8 years ago
Sebastian Junges 5d0ec15ad4 clarified error message, as the reward models are present (according to output) but simply empty
8 years ago
Sebastian Junges 9a0794fca1 refined error message wrt unexpected type of scheduler
8 years ago
TimQu e6fc962e5e In exact mode, use LP as LRA Method for nondeterministic models.
8 years ago
TimQu 87fa9908bf Fixed an issue where scheduler generation in MDPs was not possible due to end components even if there actually were no end components.
8 years ago
TimQu 0332935451 Supporting TimeOperatorFormulas for MDPs and DTMCs in Sparse, Hybrid, and Dd engine
8 years ago
TimQu b5566fa861 more on total reward formulas for mdps
8 years ago
TimQu c2dd57cda5 total rewards for mdps
8 years ago
TimQu 3310f51857 allowed for more fine grained solver requirements
9 years ago
dehnert acf297a811 fixing precision issue in sanity check and silencing min-max solver a bit
9 years ago
TimQu 51884895c8 Removed linear equation solver factories in model checkers
9 years ago
TimQu 56061c0bfa Using multiplier in MDP Model checker helpers
9 years ago
Matthias Volk 63a9f3a5ca Fixed assertion by incorporating precision
9 years ago
sjunges 7660a6c9f8 dont check != 0 in templated code
9 years ago
TimQu a1c10cac37 filtering reward zero states for MDPs
9 years ago
TimQu a2bd1e0026 renamed argument from getRequirements so that it is easier to understand
9 years ago
TimQu c59d2160ee Implemented (multi-dimensional) cost bounded properties for DTMCs (sparse engine only)
9 years ago
TimQu 149fc2e009 The solution to the minmax equation system becomes unique after eliminating end components.
9 years ago
TimQu 776ce4c8bb Checking requirements of a linear equation solver now depends on whether we want to do multiplication or equation solving. This was necessary to get the correct requirements of a MinMaxSolver that only uses the underlying linear equation solver for multiplication.
9 years ago
TimQu bb63ac6089 Linear equation solver + game solvers now respect the environment as well
9 years ago
TimQu 9771658dcc only do end component elimination in MDP model checking if there are end components
9 years ago
TimQu 42cea9c688 better subenvironments
9 years ago
TimQu 6d23c79737 Making libstorm compile again
9 years ago
TimQu fd8c99b989 Introducing Environment in MinMaxSolvers and ModelCheckers
9 years ago
TimQu d9e62a66cc cdf export for single objective formulas
9 years ago
TimQu c9beea4f33 better lower/upper result bounds
9 years ago
TimQu 86253fe88a moved multidimensional unfolding implementation from multiobjective into helper namespace
9 years ago
TimQu 117d1b5c99 clean up single objective reward bounded case
9 years ago
TimQu 016fedd58e Better progress info
9 years ago
TimQu 33585c811f MinMax Solver requirements now respect whether the solution is known to be unique or not.
9 years ago
TimQu d91d979d90 changed some output
9 years ago
TimQu 70dc9ce7ac Bypassing requirements check to make value iteration without a lower result bound work
9 years ago
TimQu e3a506ecc6 Property information output
9 years ago
TimQu 5c1de03d14 fixed min prob computation for single objective case
9 years ago
TimQu 5071df5c82 made sound value iteration work and respect the correct precision
9 years ago
TimQu 9140c1dc0e statistics and empty-epoch-matrix optimization also for single objective case
9 years ago
TimQu 23686a0f09 reward bounded cumulative reward formulas + fixes for dimensions that do not need memory
9 years ago