dehnert
208938b0a1
changed sylvan behaviour to take auto-detected number of threads if no thread count was set
8 years ago
dehnert
bcdc2a4247
added check for non-linearity to JANI menu game abstractor
8 years ago
Sebastian Junges
14be5c128f
silenced warnings about unknown pragmas in eigen and gmm wrapper
8 years ago
Tom Janson
f390aeadf3
rm broken Dijkstra from graph.cpp
8 years ago
Tom Janson
b71ef02692
comments and fixes (?) to graph.cpp's Dijkstra
This implementation seemed pretty wrong in multiple ways;
I attempted to fix it (a long time ago) (see diff, you'll see what I'm
talking about), then gave up.
Luckily (?) the code is unused, just sitting there, sad and broken.
8 years ago
Tom Janson
87e8af9852
moved ksp stuff to right location
fix include
8 years ago
dehnert
9bb65389c4
some adjustments to pgcl treatment caused by changes in JANI data structures
8 years ago
Tom Janson
6d1608a147
Dijkstra fixed, maybe
TODO: check; improve
Things that aren't going well:
- On the example graph BRP-16-2, all nodes have distance 1. I that
possible??
- The initial states list themself as their own predecessor. That's
bad, because it's simply false (unless there is a self-loop).
Former-commit-id: 06f9a28306
[formerly e7e2385e0d
]
Former-commit-id: 3505011831
9 years ago
PBerger
4feb332d55
Fixed include file
8 years ago
dehnert
bf29488219
fix for decomposition
8 years ago
dehnert
b9e4d6f334
initial support for transient boolean variables in formulas of JANI models (game-based engine)
8 years ago
dehnert
696a2e7ce1
preparing labels for JANI models (game-based abstraction)
8 years ago
dehnert
04d3a649bc
finalized location variable for JANI automata
8 years ago
dehnert
158ddc0533
equipped automata in JANI models with expression variable representing their location
8 years ago
Matthias Volk
d040e2db4b
Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation
8 years ago
dehnert
954eadc546
improved detection for early result detection in game based engine
8 years ago
dehnert
3125ad4c89
more work on boolean transient variables in JANI menu game abstraction (labels)
8 years ago
dehnert
ccf8631617
work on location support for JANI abstraction
8 years ago
dehnert
dd2fbf3d6e
fix for state set abstractor when the given predicate contains no variables
8 years ago
dehnert
d95c483a99
added location support to JANI menu game abstractor
8 years ago
dehnert
16f3b06f53
added decomposition to JANI abstractor, fixed wrong assertion
8 years ago
Sebastian Junges
c2ea78b880
no need anymore to create files from formulas if properties are present anyway
8 years ago
dehnert
45f0f1057a
fixed a bug in quantitative computation, removed debug output
8 years ago
Sebastian Junges
5c900e4e14
stats for gspn
8 years ago
Sebastian Junges
d7aa7cc7c8
expression AND with true is immediately simplified
8 years ago
Sebastian Junges
69cae73bce
fix in nextstate generator for MA
8 years ago
dehnert
b9688346cc
command decomposition working. fixed some bugs, possibly introduced more, currently debugging
8 years ago
Sebastian Junges
276261ae55
slightly more informative error message in out-of-bounds in bitvector
8 years ago
Sebastian Junges
18383f5220
several fixes in dft->gspn->jani code path: Most notably, mas are closed, successor nodes failed places keep intact and tb property is added
8 years ago
Sebastian Junges
88e17d423a
updated dft->gspn->jani workflow
8 years ago
dehnert
c03623ccea
work on command decomposition
8 years ago
dehnert
b0b1f8911e
fixed abstraction by considering related predicates for all sources. started on command decomposition
8 years ago
dehnert
2c17bdded7
fixes for JANI flattening tests
8 years ago
dehnert
df7da86bd7
flattening JANI models appears to be working, started adding tests
8 years ago
Sebastian Junges
d4f7088cfd
updates to dft->gspn
8 years ago
Sebastian Junges
0fa736d458
updated dft->gspn translation to now have basis support for spares
8 years ago
sjunges
297f3ff480
some cleaning and minor additions to dft->gspn translation
8 years ago
Sebastian Junges
faee1dfeee
updated dft->gspn translation to now have basis support for spares
8 years ago
dehnert
d6a32ca634
more work on flattening JANI compositions
8 years ago
dehnert
338bfb05c9
commit to switch workplace
8 years ago
dehnert
ae93211aeb
template edges in JANI models
8 years ago
dehnert
5aca2a432d
towards template edges
8 years ago
dehnert
1e25704c8b
commit to switch workplace
8 years ago
dehnert
be4e21d1b3
first version of jani menu-game abstraction
8 years ago
dehnert
f4146c821a
more value-reuse
8 years ago
dehnert
1552995895
improved qualitative value reuse
8 years ago
sjunges
4920eaaaea
do not allow edges with no destinations in jani
8 years ago
Sebastian Junges
f95b5f1dc0
enable shared from this does not need to be const, in particular, the constness makes python bindings for formulae impossible
8 years ago
Sebastian Junges
9d2f4ace08
additional dependent targets as imported libs created
8 years ago
Sebastian Junges
b4ce43ca0a
carl conf imported, other dependencies declared als import target and exported to storm conf
8 years ago