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
Johannes Lehmann
0d43a55923
Fixed incorrect type of modulo expression with integer inputs
4 years ago
Matthias Volk
996da02efd
Remove support for Travis CI
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
c575890229
Merge pull request #117 from tquatmann/revised-constants-comparator
Revised ConstantsComparator
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
Tim Quatmann
e1ddb9f9aa
.clang-format: disabled namespace indentation
4 years ago
Tim Quatmann
4d674e18db
Added a .clang-format file.
Co-authored-by: Daniel Basgöze
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
f0378363bb
ConstantsComparator: reduced code duplications, fixed a potentially div by 0, and silenced a warning
ConstantsComparator: The old code used `abs(x-y)/abs(x+y)<= epsilon` when comparing two numbers for equality (modulo relative precision). This is weird when x and y have different signs and potentially even causes a div by 0 whenever x=-y. Moreover the templating was awkward, causing a lot of code duplications and a Warning with clang.
Distribution[WithReward]: replaced forward declarations of ConstantsComparator by actual includes as the forward declarations caused some ambiguity regarding the template parameters.
4 years ago
Tim Quatmann
c5bbf68eaf
Removed several unnecessary forward declarations of ConstantsComparator.
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