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

5772 Commits (5c13fe624fdd0f6345a3a7670b3ed70f1c7f6fc5)

Author SHA1 Message Date
dehnert db6f43ed9d made LRA computation for deterministic systems able to respect that the underlying solver requires a fixed-point formulation
7 years ago
dehnert 86069b8552 fix typo in JSON exporter
7 years ago
dehnert 50aa6d1424 assuming the only global real transient variable is the reward when exporting JANI and no reward model is mentioned in the property (issues a warning)
7 years ago
dehnert c4bed85dc4 switching to native linear equation solver by default and power iteration
7 years ago
TimQu 1f6fc7e273 Better conversion of MA to CTMC if there are only Markovian states
7 years ago
TimQu 5a16b2befa minor fixes to let the total reward tests compile and pass
7 years ago
Matthias Volk 081c0a95d0 Export pnpro with single-server semantics
7 years ago
TimQu 1f4c0325be test cases for ctmcs and markov automata
7 years ago
TimQu 8df9b461cb total reward formulas for ctmcs and markov automata
7 years ago
TimQu b5566fa861 more on total reward formulas for mdps
7 years ago
TimQu b3edae8707 fixed fragment specification: total reward formulas should not be supported for hybrid/dd right now
7 years ago
Alexander Bork 8c3bd15eae Fixed priorities for dependencies and export of PDEP probabilities into PNPRO format
7 years ago
Matthias Volk 7dc17065c1 Updated DFT export to new JSON format
7 years ago
Sebastian Junges 0be0126095 fixed support for highlevel counterex for expected rewards in dtmcs
7 years ago
Alexander Bork 1850cf7368 Fixed trigger rates for timed transitions not being saved in .pnpro files
7 years ago
TimQu c2dd57cda5 total rewards for mdps
7 years ago
TimQu 87e34d7b32 Added Support for Total Reward Formulas for DTMCs in the Sparse Engine
7 years ago
dehnert dfc0141894 minor fix to Z3 API modification
7 years ago
dehnert cdfa328464 first attempt at adapting to Z3 interface change
7 years ago
Matthias Volk 1f221db280 Disable transformation of DFT properties to JANI
7 years ago
Matthias Volk eea940b625 Refactoring for transformation DFT->GSPN->JANI
7 years ago
dehnert 4134630fa6 adding gap output
7 years ago
Alexander Bork a49f88b7f5 Fixed computation of priorities to correctly represent the semantics
7 years ago
dehnert 4f4d1f4423 do not scale precision
7 years ago
Matthias Volk 0d4cf67f2e Set mergeDC from setting
7 years ago
Matthias Volk cf316df35e Added settings for DFT-GSPN transformation
7 years ago
Matthias Volk afb0be1245 Fixed missing dependencies to storm-parsers
7 years ago
dehnert 386f0b2e47 fixing bug in scheduler improvement step of policy iteration for games
7 years ago
Matthias Volk 369cea775d Swapped order in PriorityQueue to propagate failures in correct order
7 years ago
sjunges 8478352030 dynamic constraints and minimality labels
7 years ago
dehnert 2aff2e9382 adding some more timing output
7 years ago
sjunges 53238f43f7 fixed some missing includes due to updated API
7 years ago
sjunges 39698d6ecb fix install of storm-counterexamples
7 years ago
sjunges 79bb6734ed compile and link parsers in seperate binary
7 years ago
sjunges 3a704ae532 fix storm-dft missing includes
7 years ago
sjunges 6dfce6a405 extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times
7 years ago
dehnert b0047a5a96 improving choices in game policy iteration depending on precision of underlying solver
7 years ago
Sebastian Junges d1ab260068 remove outdated parts in highlevel counterexamplse
7 years ago
Sebastian Junges e29e6c7cd2 high level counterexamples extended with more options, and improved performance when minimizing over a subset
7 years ago
dehnert 48f5608157 making policy iteration available for game-based abstraction (prototypical for now)
7 years ago
Joachim Klein b6d67e7995 properties.cpp: Output warning if we filter away all properties
7 years ago
Joachim Klein 2948611f3f cli.cpp: Quote arguments in "Command line arguments" status line
7 years ago
Joachim Klein 04a1bbedfc properties.cpp: Log filename of properties file in --verbose mode
7 years ago
Joachim Klein 30a95ef9d6 Simplify check whether argument of --prop is a file/property
7 years ago
dehnert 9b80c65d72 more and more debugging
7 years ago
Alexander Bork fa43e515ee Changed DFT element transformation so priorities are used
7 years ago
dehnert 135c38777f game-based abstraction working with rational numbers
7 years ago
dehnert 14724b529f further debugging
7 years ago
dehnert 9f72f67d9f adding precision to less/greater in vector reduction, adding export to json
7 years ago
Matthias Volk 480b1fb8e5 Added priorities to GSPN transformation
7 years ago