tempest

Author	SHA1	Message	Date
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 It's nice to be able to copy-paste the arguments from a log file to a shell, so we'd like to have proper quoting. We thus use single quotes if an argument contains non-safe characters in the log output.	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	8 years ago
dehnert	c85e30dfd0	added distance-aware initial partition to dd-based bisimulation	8 years ago
dehnert	b415c12c25	further preparation of partial bisimulation model checker	8 years ago
dehnert	9c685f3bdb	started on partial bisimulation model checker	8 years ago
dehnert	0ef06fd31b	re-add time output to storm output and make iterative minmax solver respect linear equation solver format for policy iteration	8 years ago
dehnert	bf727a28fd	remove debug output and choose sylvan automatically in exact mode	8 years ago
Matthias Volk	349e276c9b	Removed include of cpp file in storm-pars-cli and storm-dft-cli	8 years ago
Matthias Volk	e5387ecc85	Deactivated conversion to CTMC for trivial non-determinism in MA as it is not correct at the moment	8 years ago
dehnert	e557a8e069	started on EC elimination for hybrid engine	8 years ago
dehnert	2d41de479e	added progress outputs to iterative solvers	8 years ago
TimQu	fcd277c42a	added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format	8 years ago
dehnert	68f14c728a	added missing check for existence of model	8 years ago
dehnert	b4bfd0c39f	performance improvement in DS-MPI; some cleanups	8 years ago
dehnert	df0b5fbfa5	fixed multiply-reduce operations in the presence of empty row groups	8 years ago
Sebastian Junges	e0452be54b	move some of the cli stuff to an own header	8 years ago
sjunges	e718acffba	move cli stuff from storm lib to an own small lib	8 years ago

1 2

58 Commits (5bafcbe816126f2aa0402f1e9116b04c6b21446b)