Tim Quatmann
|
3d96b0728d
|
CI: Use spot in all existing configurations. Add a new configuration without Spot.
|
3 years ago |
|
Tim Quatmann
|
e0e1b097eb
|
Merge branch 'master' into ltl-github
conflict in SchedulerGenerationMdpPrctlModelCheckerTest resolved.
Conflicts:
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
|
3 years ago |
Daniel Basgöze
|
1dab437496
|
Compare floating points upto precision instead ==
Fixes QuantileQueryTest with CLN
Provided by Tim Quatmann
|
3 years ago |
|
Daniel Basgöze
|
94ec1a7aeb
|
Fix print_storm_rational_number
|
3 years ago |
|
Daniel Basgöze
|
78a10f201e
|
Use memcpy instead of strcpy
|
3 years ago |
|
Daniel Basgöze
|
57874ff460
|
Remove C-style casts in storm_wrapper.cpp
|
3 years ago |
|
Daniel Basgöze
|
22a9703524
|
Remove erroneous mutex lock in sylvan_wrapper
Also remove trailing whitespace
|
3 years ago |
|
Daniel Basgöze
|
12111a91bd
|
Use pass-by-value in constructor
Pass by rvalue reference results in
build errors when using CLN
|
3 years ago |
|
Daniel Basgöze
|
8de8f1517a
|
Fix conversion ambiguity: Use convertNumber()
Conflicts:
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
|
3 years ago |
|
Daniel Basgöze
|
a34fcca339
|
Fix conversion ambiguity: Use 1 instead of 1.0
|
3 years ago |
|
Daniel Basgöze
|
ebd85a43d3
|
Fix conversion ambiguity: Use * instead of *=
|
3 years ago |
|
Daniel Basgöze
|
22388425d7
|
Remove unnecessary convertNumber
Fixes build errors when GMP numbers are used
|
3 years ago |
|
Daniel Basgöze
|
c6be1b6a92
|
Always define CLN_INCLUDE_DIR when available
|
3 years ago |
|
Daniel Basgöze
|
6420709a50
|
CI: Test GMP/CLN configurations and reduce tests
|
3 years ago |
|
Tim Quatmann
|
1e60fa7914
|
LTLSchedulerHelper: make handling of overlapping ECs more explicit and reduced the amount of memory states.
|
3 years ago |
|
Tim Quatmann
|
5fe81952cb
|
Removed an outdated TODO comment.
|
3 years ago |
hannah
|
6af47eaadc
|
new class for scheduler computation during LTL-MC
|
3 years ago |
|
hannah
|
8a26af29f9
|
allow HOA formulas for cslstar and pctlstar
Conflicts:
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
|
3 years ago |
|
hannah
|
63a400ea5a
|
added some documentation
Conflicts:
src/storm/storage/Scheduler.h
|
3 years ago |
|
hannah
|
133219f3c7
|
using exact fractions in tests
|
3 years ago |
|
hannah
|
0713c5dccd
|
skipDontCareStates-option for scheduler printing
Conflicts:
src/storm/storage/Scheduler.cpp
src/storm/storage/Scheduler.h
|
3 years ago |
|
hannah
|
e5b19643e8
|
dontCareStates can now be (non)deterministic and (un)defined
Conflicts:
src/storm/storage/Scheduler.h
|
3 years ago |
|
hannah
|
24ba65f5e1
|
added documentation
|
3 years ago |
|
Tim Quatmann
|
62cede1759
|
Added missing include.
|
3 years ago |
|
Tim Quatmann
|
6c7d6b0d2b
|
Silenced some unused variable-warnings.
|
3 years ago |
|
Tim Quatmann
|
396b39a21b
|
Fixed a typo (thanks @PrangerStefan)
|
3 years ago |
|
Tim Quatmann
|
4ddb9c4337
|
Some simplifications for memory structure.
|
3 years ago |
|
Tim Quatmann
|
c46c711eb7
|
cpphoafparser: added missing include.
|
3 years ago |
|
Tim Quatmann
|
693d5470a3
|
Updated changelog a bit.
|
3 years ago |
|
Tim Quatmann
|
dffc04a280
|
Cleaned up some includes for the model checkers.
Conflicts:
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
|
3 years ago |
|
Tim Quatmann
|
e92e32239b
|
Support for globally and next formulae for Markov Automata and CTMC
Conflicts:
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
|
3 years ago |
|
Tim Quatmann
|
db16aa50e6
|
LTL Helper: Removed some debug output to reduce clutter
|
3 years ago |
|
Tim Quatmann
|
a81f5e284b
|
Further simplified LTLHelper Interface a bit.
Support for LTL and HOA formulaes for *all* (sparse) model types
|
3 years ago |
|
Tim Quatmann
|
9cf3d6af5d
|
Adding debug output and file I/O checks whenever parsing a HOA automaton from a file.
|
3 years ago |
|
Tim Quatmann
|
6310462060
|
Cleaned up dtmc and mdp helpers a bit.
|
3 years ago |
|
Tim Quatmann
|
3a12b1cc10
|
Model Checkers: Reduced code duplications by using a single `computeStateFormulaProbabilities` method
Conflicts:
src/storm/modelchecker/AbstractModelChecker.h
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
|
3 years ago |
|
Tim Quatmann
|
1207af13a2
|
symbolic and sparse models now have a public member `Representation`
|
3 years ago |
|
Tim Quatmann
|
10fc5d18c8
|
Clarified what a complex path formula is.
|
3 years ago |
|
Tim Quatmann
|
b097a442ee
|
Processed some TODOs in storm/logic
Conflicts:
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
|
3 years ago |
|
Tim Quatmann
|
cdedf4e78f
|
Added comment for formula equality check. Strongly related to github issue #132.
|
3 years ago |
|
Tim Quatmann
|
c8e9b43100
|
Changed ltl2da option to slightly more descriptive ltl2datool (this is also the name of the corresponding option in PRISM)
|
3 years ago |
|
Tim Quatmann
|
948e7fdaba
|
cmake: Fixed marking non-existing option as advanced
|
3 years ago |
 Stefan Pranger
|
7a851901e2
|
updates after cherry pick
|
3 years ago |
|
Tim Quatmann
|
feadd3af77
|
Added cmake option STORM_RESOURCES_BUILD_JOBCOUNT to have better control on how many jobs we shall use to build external stuff (like spot, carl, cudd, glpk, ?)
|
3 years ago |
|
Tim Quatmann
|
98bb05b86f
|
Trying to build spot with a single thread
|
3 years ago |
|
Tim Quatmann
|
3a3587370e
|
Skip a test if LTL model checking is not available.
|
3 years ago |
|
Tim Quatmann
|
efeeea0d54
|
Spot: re-iterated cmake interface to hopefully make it more clean. Added documentation on how to update spot
|
3 years ago |
|
Tim Quatmann
|
e76c5ab4ba
|
Fixed ambiguous operator overload.
|
3 years ago |
|
Tim Quatmann
|
5a2e489403
|
github buildtest workflow should test with spot.
|
3 years ago |
|
Tim Quatmann
|
4e6d334f9b
|
Updated Changelog
|
3 years ago |
