dehnert
96539f41a5
Fixed simplification of division: division expressions must not be simplified, because it is not (yet) clear whether integer division or floating point division is to be used.
Former-commit-id: 506798c1cd
10 years ago
dehnert
5bbd85c379
Some bugfixes.
Former-commit-id: 70dcc73e91
10 years ago
dehnert
a44a3554c8
Fixed minimal command counterexample generation.
Former-commit-id: 6e7e6208da
10 years ago
dehnert
c7f262bf15
Merge branch 'mtbddIntegration' of https://sselab.de/lab9/private/git/storm into mtbddIntegration
Former-commit-id: 115d7a6c3b
10 years ago
dehnert
00e7121bc4
some work towards BDD-based mc.
Former-commit-id: cae0c4421e
10 years ago
dehnert
546e047b8d
Fixed a bug that prevented correct comparison with bounds in formulas.
Former-commit-id: ae6c28dcbe
10 years ago
dehnert
3fd62bc697
More work on MTBDD-based mc.
Former-commit-id: 52081fc741
10 years ago
dehnert
0c2080f220
Added tests for sparse Prob0/1 to functional tests
Former-commit-id: ef8f9ffb59
10 years ago
dehnert
81100c7afd
debugged and added more tests for prob0/1 for MDPs using BDDs
Former-commit-id: f47fb3631a
10 years ago
dehnert
c70d93f4d3
Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.
Former-commit-id: 3215a38c44
10 years ago
dehnert
7e14dc031b
Reverted the last commit. The flag is there for performance reasons and there is no reason why it shouldn't work that way.
Former-commit-id: e551eb461f
10 years ago
masawei
97936cbd8e
Found a fix for a bug causing the functional tests to segfault at DeterministicModelBisimulationDecomposition.Die.
- By setting the blocks to be not sorted and unique a different constructor is used by the boost container. This prevents the segfault.
|- I can't say exactly why this works nor do I know if the blocks are actually sorted and unique in the sense meant by the underlying container implementation.
Former-commit-id: a1bfbab75a
10 years ago
dehnert
923007cdc3
Merge branch 'master' into mtbddIntegration
Former-commit-id: 1fdddfbd8c
10 years ago
dehnert
bda8d63b3b
Merge master into mtbddIntegration.
Former-commit-id: ad1ab84439
10 years ago
David_Korzeniewski
7d2d1cac55
Functional Testing Suite now prints a note if not all optional dependencies were included in the build.
Former-commit-id: 36974ebb66
10 years ago
David_Korzeniewski
95d5ebbb7d
Updated build instructions with list of tested compilers and some new dependencies, but it still looks partially outdated.
Former-commit-id: 1931f71cf9
10 years ago
dehnert
1a1906f811
Added functional tests for DD-based and sparse computation of states with prob 0 and 1.
Former-commit-id: a62c67c657
10 years ago
dehnert
c8007876ae
Symbolic models can now be built from the command line.
Former-commit-id: 2c239df754
10 years ago
dehnert
239caf57eb
Added symbolic models and made DD-based model generator build the correct instances.
Former-commit-id: c054401cfd
10 years ago
dehnert
8a906038f6
Added reward model generation for DD-based model builder.
Former-commit-id: 4837cf9229
10 years ago
dehnert
7c2f60175e
Intermediate commit: fixed parsing bug and started reward generation (DD).
Former-commit-id: a27c815831
10 years ago
dehnert
f0b174b756
Fixed performance tests.
Former-commit-id: f58e2eb923
10 years ago
dehnert
a1dae8849e
Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented.
Former-commit-id: d4e6df30b5
10 years ago
David_Korzeniewski
4dc69dd6f5
Fixed performance tests, and again things concerning templates I never heard of before.
Former-commit-id: 1d110c6aad
10 years ago
David_Korzeniewski
7515ca5293
Fixed compile errors caused by parts of the c++ standard I've never heard of before...
Former-commit-id: 8dbd813f42
10 years ago
David_Korzeniewski
8ebc0e4640
Final touches on cuda nondeterministic linear equation solver & modelchecker
Former-commit-id: c549ae0401
10 years ago
David_Korzeniewski
b623384dda
Fixed merge errors and adapted to changes in master
Former-commit-id: 08054e7bec
10 years ago
David_Korzeniewski
3936470b11
Merge branch 'master' into cuda_integration
Conflicts:
src/settings/SettingsManager.cpp
src/settings/modules/GeneralSettings.cpp
src/settings/modules/GeneralSettings.h
src/storage/StronglyConnectedComponentDecomposition.cpp
src/utility/cli.h
Former-commit-id: ff76ae68d5
10 years ago
David_Korzeniewski
ea2e616196
All tests for CUDA based TopologicalValueIterationMdpPrctlModelChecker passing on Windows.
Former-commit-id: 68cafa6f84
10 years ago
dehnert
706ea56963
Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster.
Former-commit-id: 07ffb5882d
10 years ago
dehnert
e79233bd7b
Added check in PRISM program that prevents global varibles from written in possibly synchronizing commands.
Former-commit-id: 34e34cacbe
10 years ago
dehnert
3977cafe73
Extended DD-based model building to also build the MDP models of our benchmark suite. Added (MDP) tests for DD-based model building and explicit model building.
Former-commit-id: 4e18f98ee6
10 years ago
dehnert
8c1870eb54
Intermediate commit.
Former-commit-id: e5f251718f
10 years ago
dehnert
0f0baf61a4
Made DD-based model construction work for all DTMC benchmarks we have. Included tests for both DD-based and excplicit model generation from PRISM models.
Former-commit-id: e4af6d9f8a
10 years ago
dehnert
b3d18c2367
Enabled probabilities depending on source state variables.
Former-commit-id: 8c12ac975c
10 years ago
dehnert
7d1829aefa
More work on DD-based model generation.
Former-commit-id: f6f37bd521
10 years ago
dehnert
e58d38fadf
More work on integrating DD-based model building.
Former-commit-id: 84f5a5c603
10 years ago
dehnert
6347e19da8
Intermediate commit: integrating MTBDD model generation/model checking to main tool.
Former-commit-id: a312d3a425
10 years ago
dehnert
c3c83fbe4f
Fixed some compilation errors.
Former-commit-id: dc626450b8
10 years ago
dehnert
e89e089754
Removed parametric main files.
Former-commit-id: 526f0754bb
10 years ago
dehnert
f0b591be77
Further work on reintegrating parametric model checking into main executable.
Former-commit-id: be95ce2722
10 years ago
dehnert
53b77e673b
Fixed a minor issue.
Former-commit-id: 7df7a0b38f
10 years ago
dehnert
5794bbea56
Made some adaptions to make parametric model checking work in the main executable.
Former-commit-id: 0f56bec3e2
10 years ago
dehnert
caf8b57b60
Started integrating parametric model checking in regular tool.
Former-commit-id: e647e0bbe6
10 years ago
dehnert
0a2d079c3a
Merge master in parametricSystems.
Former-commit-id: 2d952c21dc
10 years ago
dehnert
56ea5fca14
Included move-construction and move-assignment for partition.
Former-commit-id: 8ed399c308
10 years ago
David_Korzeniewski
00ddce497d
corrected identifier name.
One should actually read documentation, not just look at it...
Former-commit-id: 69d8154496
10 years ago
David_Korzeniewski
4b44e625d0
Adapted Death-Tests in BitVectorTest.cpp to return codes upon assertion failure on Windows and deactivate them everywhere if the macro NDEBUG is defined (as that disables assertions)
Former-commit-id: be04a49e57
10 years ago
David_Korzeniewski
e41922347d
Adapted ExpressionTest.cpp to weird behavior of windows when using temporary shared_ptr in make_pair in initializer_list.
Now using const_pointer_cast instead of static_cast to modify shared pointers. (Although it worked with static_casts, but you never know)
Former-commit-id: d42487bb0c
10 years ago
David_Korzeniewski
07ddaa314c
User declared move constructor and move assignment, as they are currently required to ensure pointer validity.
Former-commit-id: 5e239c60cc
10 years ago