Matthias Volk
|
d3c8093e0f
|
Removed unnecessary semicolons
|
5 years ago |
|
Matthias Volk
|
f45db73afe
|
Support coloured output for GCC
|
5 years ago |
Tim Quatmann
|
a187a299af
|
Merge branch 'master' into prism-pomdp
|
5 years ago |
|
Tim Quatmann
|
5a221acbd0
|
Multi-objective model checking: Fixed incorrect computations for some models with end components. (Github Issue #75)
|
5 years ago |
|
Tim Quatmann
|
08c60bcb3d
|
Added OVISolverSettings to storm-pomdp
|
5 years ago |
Sebastian Junges
|
c0ac9814e1
|
allow for graph-analysis and sat-based analysis interleaving, and restarting sat-based solver when advantageous
|
5 years ago |
|
Sebastian Junges
|
ea73e246a7
|
A new qualitative reachability analysis for POMDPs/prob1max, based on graphs (sound but incomplete).
|
5 years ago |
|
TimQu
|
7504f6f315
|
Improved statistics output for refinements, added detection of fixpoints
|
5 years ago |
|
Tim Quatmann
|
5a76f7355d
|
Fixed an issue with refinement of under-approximation
|
5 years ago |
|
Tim Quatmann
|
16ad9d3a83
|
fixed storm-pomdp output a little.
|
5 years ago |
|
Tim Quatmann
|
96309e1f11
|
Merge branch 'master' into prism-pomdp
|
5 years ago |
|
Tim Quatmann
|
4eed592811
|
--timeout now just sends a SIGALRM signal (which can be catched by the signal handler).
|
5 years ago |
|
Tim Quatmann
|
8b4595042e
|
Only do iteration output if the result bound improved. Handle integer overflows for the observation resolution.
|
5 years ago |
|
Sebastian Junges
|
a5774cf2bd
|
Merge branch 'master' into almostsurepomdp
|
5 years ago |
|
Sebastian Junges
|
4930908942
|
new version of containsVariable, with better performance and somewhat better to debug
|
5 years ago |
|
Sebastian Junges
|
91cad8164f
|
trace outputs towards debugging the JaniScopeChanger
|
5 years ago |
|
Sebastian Junges
|
e4a4214fc4
|
towards more helpful output when POMDP is not canonical
|
5 years ago |
|
Sebastian Junges
|
0e97647d9e
|
canonic POMDPs are now annotated with the state valuations and the choice labellings
|
5 years ago |
|
Sebastian Junges
|
5277139640
|
first version of a generator for belief support MDPs
|
5 years ago |
|
Sebastian Junges
|
94c87a9926
|
first version of query interface that is more accessible than the winning region itself
|
5 years ago |
|
Sebastian Junges
|
86ece9d324
|
cleaning code
|
5 years ago |
|
Tim Quatmann
|
43220759f4
|
Implemented a time limit for exploration.
|
5 years ago |
|
Tim Quatmann
|
e81b8f1622
|
BeliefManager: fixed a few assertion conditions
|
5 years ago |
|
Tim Quatmann
|
c91c98f2de
|
Pomdp: Fixing result output with exact numbers
|
5 years ago |
|
Tim Quatmann
|
1763f0c582
|
Making sure that we only store the best bounds found so far. Also added some output for the resulting values in each iteration.
|
5 years ago |
|
Tim Quatmann
|
fa624d2a20
|
Introduced new settings for controlling the refinement strategy and whether to produce only upper and/or lower bounds
|
5 years ago |
|
Tim Quatmann
|
2d94e77f2a
|
Only display the bound that was requested.
|
5 years ago |
|
Tim Quatmann
|
6dd50575f9
|
New 'belief-exploration' setting (replaces gridapproximation setting)
|
5 years ago |
|
Tim Quatmann
|
37490a8eca
|
Started to integrate new refinement options.
|
5 years ago |
|
Tim Quatmann
|
45f9c66602
|
Merge branch 'master' into prism-pomdp
|
5 years ago |
|
Tim Quatmann
|
a728c01322
|
BitVector: Fixed an issue with the move assignment operator. The 'other' BitVector was left in an invalid state.
|
5 years ago |
|
Tim Quatmann
|
75d792e987
|
Implemented refinement heuristic.
|
5 years ago |
|
Tim Quatmann
|
45832d3de3
|
BeliefMdpExplorer: Implemented extraction of optimal scheduler choices and reachable states under these choices
|
5 years ago |
|
Tim Quatmann
|
61215e4b24
|
Over-Approximation: Taking current values as new lower/upper bounds for next refinement step.
|
5 years ago |
|
Tim Quatmann
|
4ea452854f
|
Fixes for scoring observations
|
5 years ago |
|
Matthias Volk
|
7e1f5bf2ac
|
Fixed handling of constant BE in approximation
|
5 years ago |
|
Matthias Volk
|
49dac54e8b
|
Fixed typos
|
5 years ago |
|
Tim Quatmann
|
d5bcec11e3
|
Merge branch 'master' into prism-pomdp
|
5 years ago |
|
Tim Quatmann
|
88c31b36d0
|
Equation system based CTMC LRA solving: For the 'inner' linear equation system solver, also set whether the solver type has been set from default. This avoids potentially using unsound/inexact equation solvers.
|
5 years ago |
|
Tim Quatmann
|
1a00b4d22d
|
Merge remote-tracking branch 'origin/master' into prism-pomdp
|
5 years ago |
Daniel Basgöze
|
7076a54dfb
|
Add error checking to C style io
|
5 years ago |
|
Daniel Basgöze
|
b7c53c080b
|
Remove trailing whitespace
|
5 years ago |
|
Daniel Basgöze
|
002d9e1925
|
Add error checking to C style io
|
5 years ago |
|
Daniel Basgöze
|
1ee87a876a
|
Remove trailing whitespace
|
5 years ago |
|
Daniel Basgöze
|
92f25c1fa7
|
Use standard integer types instead of size_t
|
5 years ago |
|
Daniel Basgöze
|
a244b5ff67
|
Add assertion for an implied limitation
|
5 years ago |
|
Daniel Basgöze
|
d62af9332b
|
Fix bitshift overflow
The simple 1 is a 32bit integer literal on most machines leading to an
overflow: 1<<32 == 0. Even on 64 bit machines.
|
5 years ago |
|
Daniel Basgöze
|
64e70c406e
|
Replace size_t with uint64_t in bitoperations
|
5 years ago |
|
Daniel Basgöze
|
aa0fe082d7
|
Document bitoperations.h
|
5 years ago |
|
Daniel Basgöze
|
972abfcf6f
|
Include required headers
|
5 years ago |
