Sebastian Junges
|
2cd25d069c
|
To dice translation, remove hack for modulo
|
4 years ago |
Sebastian Junges
|
d144a1776c
|
prism next state generator, rename actions to reflect labeled choices vs unlabeled choices are sync vs async
|
4 years ago |
Sebastian Junges
|
3f165785d0
|
integrated feedback on code quality by TQ
|
4 years ago |
Sebastian Junges
|
4c350b3e2d
|
print predicate expressions added
|
4 years ago |
Sebastian Junges
|
b3a69e24a3
|
Update src/storm/storage/prism/OverlappingGuardAnalyser.h
Co-authored-by: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
|
4 years ago |
Sebastian Junges
|
f3c54a06a1
|
Simplify assertion
(thanks to Tim)
Co-authored-by: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
|
4 years ago |
Sebastian Junges
|
6d7802975f
|
remove compilation error and improve associated feedback to user
|
4 years ago |
Sebastian Junges
|
a9fbbab447
|
premerge changelog cleanup
|
4 years ago |
Sebastian Junges
|
76bf1049ee
|
test for masking during building
|
4 years ago |
Sebastian Junges
|
ed25e903b7
|
exportexplicit test case added
|
4 years ago |
Sebastian Junges
|
6ce1f96efc
|
belief support tracking test and cleaning
|
4 years ago |
Sebastian Junges
|
796b76b242
|
jani-belsupmc tests added
|
4 years ago |
Sebastian Junges
|
01bd04b170
|
test cases for iterative qualitative added
|
4 years ago |
Sebastian Junges
|
4844573b63
|
qualitative search: oneshot cleaning and tests
|
4 years ago |
Sebastian Junges
|
6b5c7b2672
|
minimal test cases for qualitative analysis: graphs
|
4 years ago |
Sebastian Junges
|
f77e8b2dc2
|
added a minimal test for makecanonic
|
4 years ago |
Sebastian Junges
|
9e2bc9b341
|
testing for writing to global vars from action-labelled models
|
4 years ago |
Sebastian Junges
|
271fdb0607
|
minimalistic test cases for building POMDPs added
|
4 years ago |
Sebastian Junges
|
922d6f6572
|
export of compressed states to json with negative values fixed
|
4 years ago |
Sebastian Junges
|
f910288aea
|
global command indices may not be from 0 to N, so we have to check for highest command index explicitly
|
4 years ago |
Sebastian Junges
|
f43cb6a798
|
fix testfile
|
4 years ago |
Sebastian Junges
|
31d8fb33e8
|
Merge remote-tracking branch 'publicdev/almostsurebdd'
|
4 years ago |
Sebastian Junges
|
b9bd9e2fd4
|
parser test for nary predicates
|
4 years ago |
Sebastian Junges
|
a4e8d9ea11
|
post-merge fix to when substituting predicates and unbounded integers
|
4 years ago |
Sebastian Junges
|
f419c3aac0
|
Merge branch 'master' of https://github.com/sjunges/storm
|
4 years ago |
Sebastian Junges
|
60ed3c74e7
|
update changelog to reflect branch merge
|
4 years ago |
Tim Quatmann
|
decd3e0ad8
|
Merge pull request #115 from AlexBork/master
Fix for CUDD
|
4 years ago |
Alex Bork
|
db9097be8c
|
Fix for CUDD
|
4 years ago |
Sebastian Junges
|
cf63ea6767
|
eliminate nonstandard predicates early on
|
4 years ago |
Sebastian Junges
|
58e1cc6af0
|
extend prism maze example with bad state
|
4 years ago |
Tim Quatmann
|
bc506d24f1
|
Merge pull request #114 from tquatmann/prism-unbounded-integers
Support for Prism Programs with unbounded integers
|
4 years ago |
Sebastian Junges
|
bbbe178572
|
Cleaning and support for linux platforms
|
4 years ago |
Sebastian Junges
|
f841e75679
|
Merge branch 'prismlang-sim' into almostsurebdd
|
4 years ago |
Sebastian Junges
|
85b676ff57
|
better output
|
4 years ago |
Sebastian Junges
|
65ba87dbd0
|
removed debug output
|
4 years ago |
Sebastian Junges
|
1218991e6a
|
can switch off producing schedulers in the instantiation model checker
|
4 years ago |
Tim Quatmann
|
a7a10136fa
|
Cmake: Marking two options as advanced.
|
4 years ago |
Tim Quatmann
|
b3a6d91d58
|
CMake: Changed github address of Carl.
|
4 years ago |
Tim Quatmann
|
a07ee8a018
|
Updated Changelog
|
4 years ago |
Tim Quatmann
|
bdd89d87b2
|
Prism next state generator now deals with unbounded integer variables.
|
4 years ago |
Tim Quatmann
|
1fe0254f5d
|
DdPrismModelBuilder now errors in case it has a program with unbounded integer variables as input
|
4 years ago |
Tim Quatmann
|
9f1c540f05
|
Counterexamples:making minimal label set generator aware of unbounded integer variables
|
4 years ago |
Tim Quatmann
|
171ff270e0
|
Prism to Jani conversion now supports unbounded integer variables
|
4 years ago |
Tim Quatmann
|
8f9ff95531
|
Added Test cases for parsing/processing prism programs that use unbounded integer variables
|
4 years ago |
Tim Quatmann
|
5c2b9c503c
|
prism/Program: Integer variables can now have no lower and/or upper bound.
|
4 years ago |
Tim Quatmann
|
aa5bb9cb7d
|
PrismParser: Parsing unbounded integer variables
|
4 years ago |
Tim Quatmann
|
871efc0d8c
|
Fixed TerminalStatesGetter with multi-bounded formulae.
|
4 years ago |
Daniel Basgöze
|
b58addcf50
|
Github Actions: fix PR testing originating from different branches
|
4 years ago |
Daniel Basgöze
|
b6c8ab1cf6
|
Github Actions: use current ref instead of hardcoded master
|
4 years ago |
Tim Quatmann
|
aac792bd1d
|
Updated list of contributers in Readme
|
4 years ago |