620ef30529
Merge branch 'master' into cli_refactoring
8 years ago
f5c327a10e
Boost must be set for shipped carl
8 years ago
ea02ea0838
started overhaul of cli/api
8 years ago
b76ee0210a
Fixed setting cmake flags for building shipped carl
8 years ago
b695dd48fb
Fixed assertion to allow timebound 0
8 years ago
a9d6d80ef0
Warning in cmake if Z3 is not found
8 years ago
aa158f5144
ContinuousToDiscreteTimeModelTransformer can now transform the model out-of-place as well
8 years ago
13982b4116
Merge branch 'choicelabels'
8 years ago
433c05cc3e
Fixed compiling under Linux
8 years ago
790ae46e4f
Fixed explicit dft model builder.
8 years ago
0cdd32ff9f
added two test cases for the drn parser
8 years ago
9f894667eb
Fixed DRN exporter/parser: MAs are not supported as there is no indication for Markovian choices
8 years ago
36b38b10ee
fixed smt minimal command set generator
8 years ago
8a3c9a3184
Merge remote-tracking branch 'origin/master' into choicelabels
8 years ago
8e26ceda5c
fixed incorrect return value of isDeterministicModel
8 years ago
f2ab549b36
fixed compiling storm-dft
8 years ago
b4ad2718b0
fixed parser tests
8 years ago
e7a8357ee6
Fixed some tests
8 years ago
88fc7fda0c
fixed tests that used the prism model builder (reverted from commit f762491ce4)
8 years ago
576f92568e
StateValuations and ChoiceOrigins are now members of a sparse::Model.
A model can now be constructed by providing a modelComponents struct.
8 years ago
464bdc389c
improved state valuations class
8 years ago
e7e4486cf4
Merge remote-tracking branch 'origin/master' into choicelabels
8 years ago
1ce122a0d6
fixed compile issue related to ambiguous call of operator<<
8 years ago
a8e877d016
fixed capitalization.
8 years ago
722e67fe64
parsing choice labels for explicit models
8 years ago
f558cb866c
using exact data types for smt-based multi objective model checking tests. Also disabled a few tests that test (yet) unsupported queries or that take too long.
8 years ago
1d329176ba
Resolved compiling issues due to recent merge
8 years ago
8dfa141a4a
Exporting .dot for explicit input.
removed duplicated code for explicit input with parametric engine
8 years ago
77a90184e7
building choice labeling when the corresponding option is given
8 years ago
cd5ee63cce
fixed preserving the choice labeling when an ma is closed
8 years ago
dc079b3196
moved a function to graph.h
8 years ago
7c90e1e6c2
Merge remote-tracking branch 'origin/smt-based-multi-objective'
8 years ago
58fad65ab6
fixes for the string representations of prism choice origins
8 years ago
b531dccad9
.dot output for deterministic models with choice labels
8 years ago
e7bc5fdef9
fixed several minor bugs regarding the choicelabeling
8 years ago
bf97d79573
moved building the choice origin strings into the ChoiceOrigins class
8 years ago
7e5bb4aa0e
Merge remote-tracking branch 'origin/master' into choicelabels
8 years ago
0aed35f4b4
worked on human readable representations of prism command sets
8 years ago
db31c1cb11
improved .dot export of models with choice labeling
8 years ago
6537fd8b72
Replaced the old choice labeling with the new one and used choice origins for the minimal command set counterexample generators
8 years ago
a067527aa0
As pointed out by Joachim Klein, weak bisimulation does not preserve reward properties. Therefore, weak bisimulation now refines blocks with non-zero reward wrt. strong bisimulation.
8 years ago
c5d0b281ce
fixed a recently introduced bug affecting entry counts in explicit reward matrices
8 years ago
89454481d0
Merge pull request #4 from ArashPartow/master
Minor updates to ExprTk
8 years ago
70ebe36ec6
adapted tests to recent changes wrt to 0-transition insertions in explicit parser
8 years ago
9bc55e3107
Merge remote-tracking branch 'origin/master' into choicelabels
8 years ago
f762491ce4
fixed tests that used the prism model builder
8 years ago
759e351e95
Improved explicit model building:
- There is now an option to generate a choice labeling that corresponds to the specified action names.
- The old choice labeling (where each choice was labeled with an index set representing the corresponding prism commands) is renamed to choiceOrigins and has been improved towards support of other input formats (such as Jani) and other applications such as scheduler synthesis
8 years ago
c595fee4dc
removed some unnecessary transition insertions in parser
8 years ago
cb90600abb
Silenced a warning
8 years ago
25074b50a9
Added function to get the next unset bit in a bitvector
8 years ago
dehnert
Matthias Volk
TimQu
TimQu
cdehnert