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

70 Commits (1e3686480a63b1fa2baa601c31732d66e13765f9)

Author SHA1 Message Date
TimQu b6a5fcfd84 Settings: Do not hard-code executable name in help message.
6 years ago
TimQu d6e91183d7 cli: don't print the whole help message when an error occurred during option parsing.
6 years ago
Tim Quatmann 3a11a4b3eb Introducing a TBB adapter that #undefs TRUE and FALSE.
6 years ago
TimQu eb15177801 cli: try to recover after checking a property has failed. (related to GitHub issue #42)
6 years ago
Tim Quatmann 80bfa6b56e Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set.
6 years ago
Matthias Volk 87d078f897 Output error by STORM_LOG_ERROR
6 years ago
TimQu c1119fcd8d Triggered conversion from PRISM to JANI when building an MA with the dd engine since MAs are unsupported in the DdPrismModelBuilder.
6 years ago
TimQu 19f353591f Added an option to transform CTMCs to MAs and DTMCs to MDPs.
6 years ago
TimQu 02977da3d7 Apply maximum progress assumption while building a Markov Automaton explicitly.
6 years ago
TimQu c27b8af90f Display the time required for parsing the prism/jani input
6 years ago
TimQu 0434d9f83a fixed issue when checking whether transition rewards can be lifted
6 years ago
dehnert e745ddbe0d some fixes related to DD-based JANI model building
6 years ago
TimQu bf40fb54f2 added api call that directly applies a given jani-property filter
6 years ago
TimQu 019cc8b1a0 preserved order of jani-properties as given in the file
6 years ago
TimQu 31a67afa4a also print filtered rationalNumber checkresults as double
6 years ago
TimQu ee9e6354a3 removed standard-compliant option: storm-conv now produces standard compliant jani code by default
6 years ago
TimQu 55efedb713 prism2jani no longer fails if a reward model has the same name as a formula/variable
6 years ago
TimQu 101b49b898 detect unsupported jani-features directly upon parsing the model.
6 years ago
TimQu c739f0befa elimination of jani function
6 years ago
TimQu 2febe36a65 removed dependency on storm-conv
6 years ago
TimQu 7c61a16d91 fixes for array expressions, support to translate properties that consider array expressions, translating array models in cli
6 years ago
dehnert 6ab7859c84 fixing more of Lindas issues
6 years ago
dehnert 51be532695 pulled out parsing from abstraction-refinement classes
6 years ago
TimQu 8050f8fc67 eliminate reward accumulations on jani level
7 years ago
TimQu 831f07e867 eliminate reward accumulations whenever possible
7 years ago
TimQu 910b6e6b22 fixed wrong include
7 years ago
TimQu 0fa361c393 displaying property name together with the property
7 years ago
TimQu 35aa166f5b added possibility to check all available jani properties
7 years ago
TimQu 86f0195b18 removed jani conversion in cli of main binary
7 years ago
dehnert 9d528db2fc adding translation of expressions used in formulas to symbolic-to-sparse transformers
7 years ago
TimQu 0c0f61e27b Fix: Only access counterexample settings in model-handling, if they are available.
7 years ago
Sebastian Junges 0be0126095 fixed support for highlevel counterex for expected rewards in dtmcs
7 years ago
sjunges 79bb6734ed compile and link parsers in seperate binary
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
Joachim Klein 2948611f3f cli.cpp: Quote arguments in "Command line arguments" status line
7 years ago
Matthias Volk 99e5619952 Export storm targets
7 years ago
Sebastian Junges 61925d1c98 add option for sparse model builder to add a state encoding out-of-bounds state valuations to enable analysis of buggy models
7 years ago
dehnert 21c970f8f7 added dd-to-sparse engine that builds the model as a DD and then transforms the whole model to a sparse representation
7 years ago
dehnert 09866e4577 enabling changing value type in quotient extraction of dd-bisimulation
7 years ago
dehnert 5f7cd17789 added printing info when value type is converted after preprocessing
7 years ago
dehnert 139752eb66 added option to perform dd-bisimulation using exact arithmetic
7 years ago
dehnert 9e5e1980dd first working version of symbolic Markov automaton bisimulation
7 years ago
dehnert 4d7be96dda MaxSAT-based high-level counterexamples for JANI
7 years ago
dehnert 24d6337006 JANI choice origins and MILP-based high-level cex for JANI
7 years ago
dehnert 4591dba631 made maxsat-based counterexample generation be applicable to DTMCs and MDPs
7 years ago
dehnert 0d18886966 re-enabling conversion of MA to CTMC if the MA only has Markovian states
7 years ago
sjunges 12dda40919 split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs
7 years ago
dehnert c85e30dfd0 added distance-aware initial partition to dd-based bisimulation
7 years ago
dehnert b415c12c25 further preparation of partial bisimulation model checker
7 years ago
dehnert 9c685f3bdb started on partial bisimulation model checker
7 years ago