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

130 Commits (e156d7b8e798141f7a86638cc13dcbc905b73835)

Author SHA1 Message Date
Matthias Volk b8991ca4bf Fixed compile issue due to merge
6 years ago
Matthias Volk e4e069a98c Slight refactoring of transformations
6 years ago
TimQu 9438d56ab3 added cli option for transforming continuous time models to discrete time.
6 years ago
Tim Quatmann a47945a931 Cleaner output when exporting schedulers
6 years ago
Tim Quatmann 72425ec1b2 CLI: Added an option to export the produced scheduler to a file.
6 years ago
Alexander Bork 450e074c5b Integrated non-Markovian state elimination into Storm MA modelchecking
6 years ago
Sebastian Junges d295f6e777 export of bdds into dot and text format
6 years ago
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.
7 years ago
TimQu 19f353591f Added an option to transform CTMCs to MAs and DTMCs to MDPs.
7 years ago
TimQu 02977da3d7 Apply maximum progress assumption while building a Markov Automaton explicitly.
7 years ago
TimQu c27b8af90f Display the time required for parsing the prism/jani input
7 years ago
TimQu 0434d9f83a fixed issue when checking whether transition rewards can be lifted
7 years ago
dehnert e745ddbe0d some fixes related to DD-based JANI model building
7 years ago
TimQu bf40fb54f2 added api call that directly applies a given jani-property filter
7 years ago
TimQu 019cc8b1a0 preserved order of jani-properties as given in the file
7 years ago
TimQu 31a67afa4a also print filtered rationalNumber checkresults as double
7 years ago
TimQu ee9e6354a3 removed standard-compliant option: storm-conv now produces standard compliant jani code by default
7 years ago
TimQu 55efedb713 prism2jani no longer fails if a reward model has the same name as a formula/variable
7 years ago
TimQu 101b49b898 detect unsupported jani-features directly upon parsing the model.
7 years ago
TimQu c739f0befa elimination of jani function
7 years ago
TimQu 2febe36a65 removed dependency on storm-conv
7 years ago
TimQu 7c61a16d91 fixes for array expressions, support to translate properties that consider array expressions, translating array models in cli
7 years ago
dehnert 6ab7859c84 fixing more of Lindas issues
7 years ago
dehnert 51be532695 pulled out parsing from abstraction-refinement classes
7 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