c7b83ffb5f
moved parameter lifting related code out of the main library/executable
9 years ago
6ef8cf3042
Fixed compile problem with ull
9 years ago
c28aebd52b
improved output of scheduler a little
9 years ago
2f49255db6
Improved storage::Scheduler. We can now consider arbitrary finite memory schedulers, potentially employing randomization.
9 years ago
16041bc936
Improved memory structure so that a memory update is triggered based on the transition that was taken (and not only the state that was reached)
9 years ago
35c9b58fda
added a test case for SparseMatri::restrictRows and fixed it
9 years ago
3fd72a11d8
Improved SparseMatrix::restrictRows so it can handle empty row groups
9 years ago
ea02ea0838
started overhaul of cli/api
9 years ago
aa158f5144
ContinuousToDiscreteTimeModelTransformer can now transform the model out-of-place as well
9 years ago
433c05cc3e
Fixed compiling under Linux
9 years ago
790ae46e4f
Fixed explicit dft model builder.
9 years ago
8e26ceda5c
fixed incorrect return value of isDeterministicModel
9 years ago
e7a8357ee6
Fixed some tests
9 years ago
576f92568e
StateValuations and ChoiceOrigins are now members of a sparse::Model.
A model can now be constructed by providing a modelComponents struct.
9 years ago
f0f4cd7390
first version of sparse quotient extraction for dd bisimulation
9 years ago
464bdc389c
improved state valuations class
9 years ago
58fad65ab6
fixes for the string representations of prism choice origins
9 years ago
e7bc5fdef9
fixed several minor bugs regarding the choicelabeling
9 years ago
bf97d79573
moved building the choice origin strings into the ChoiceOrigins class
9 years ago
0aed35f4b4
worked on human readable representations of prism command sets
9 years ago
6537fd8b72
Replaced the old choice labeling with the new one and used choice origins for the minimal command set counterexample generators
9 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.
9 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
10 years ago
25074b50a9
Added function to get the next unset bit in a bitvector
10 years ago
4413afb542
used new helper functions at some points in the code
10 years ago
8a7609fb83
fixed Rmin computation with exact sparse engine when very high rewards occur
10 years ago
7f346d2f0b
more work on quotient extraction
10 years ago
d655621ea1
Fixed seg fault when building model valuations
10 years ago
8f42bd2ec0
moved to new sparsepp version and made the appropriate changes
10 years ago
ef90b1b224
Fix for memory structure product and toString method
10 years ago
c5f29c3761
Fixes and improvements for memory structure
10 years ago
6a3310f7ee
Improved Jani-to-dot:
- Fixed problems when the model name contained a dot
- Edges are displayed nicer
- Action names are displayed.
10 years ago
291f5ecd47
First version of Jani-to-Dot.
10 years ago
697ae21b6f
Suppress warning
10 years ago
586929ea64
As we do not support windows, we can also get rid of:
#ifndef WINDOWS
especially since the guards were around move-constructors, which are supported under Windows since Visual Studio 2015
10 years ago
fc97c1fc9d
introduced memory structure
10 years ago
3f9aa29db2
Fixed compilation with gmp as rationalNumber/ rationalFunctionCoefficient
10 years ago
28e91b8d0f
more work on symbolic bisimulation
10 years ago
43fdf0a89b
Fixed a couple of warnings
10 years ago
03ad4c2783
first version of symbolic bisimulation minimization
10 years ago
970b72786c
disable level simplification for now
10 years ago
bae4b421ab
added missing template instantiation and print more info on LTO in cmake
10 years ago
c16390e7f5
Equality Comparisons for JaniVars, just to make life easier :-)
10 years ago
c5c14f3178
extended JSONExporter to properly export non-constant time/step intervals
10 years ago
f0ae3a2dfb
Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N
10 years ago
cde59bd436
added Expression::evaluateAsRational
10 years ago
dd40254628
PLA for continuous models
10 years ago
153339c5be
first draft of policy iteration using DDs
10 years ago
952776a057
hybrid engine working for rational numbers
10 years ago
ee90c51b2a
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
10 years ago
TimQu
Matthias Volk
dehnert
Sebastian Junges
sjunges