dehnert
f7a578e65d
Major change in PRISM grammars and IR: the IR now uses unique pointers instead of shared pointers to express ownership of objects more clearly.
Former-commit-id: 5b0228ee3b
11 years ago
dehnert
20ae92e1ba
Added support for cloning IR expressions.
Former-commit-id: 913269b3a5
11 years ago
dehnert
2cc5b6e080
Added Z3ExpressionAdapter to translate IR expressions to the Z3 format. Improvements to label-/command set generators. Disabled MILP-call from main().
Former-commit-id: 7128ab4477
11 years ago
dehnert
bd3edb5f8b
Naive enumeration of command set works.
Former-commit-id: 45466d1edc
11 years ago
dehnert
a7dda9131b
Intermediate commit to switch workplace.
Former-commit-id: 2ade4ee21f
11 years ago
dehnert
e3234b54f3
Step towards minimal command generator using MaxSAT and model checking.
Former-commit-id: 4237447c44
11 years ago
dehnert
f33bf69daa
Another merge.
Former-commit-id: 00450616d1
11 years ago
dehnert
2e570f6311
Merge.
Former-commit-id: 572cdb80fc
11 years ago
dehnert
623d9ee7c4
Added capability to restrict model to certain action choices.
Former-commit-id: fb3c63c64f
11 years ago
dehnert
121cbb7610
ExplicitModelAdapter now labels updates for synchronizing commands correctly.
Former-commit-id: ae9e6c9bda
11 years ago
dehnert
a45e9423b8
Sparse matrix can now also be used without knowing the number of rows/columns/nonzeros upfront. Adapted ExplicitModelAdapter to use that capability to not explore the state space twice. Added support for Z3 to CMakeLists.txt. Added correct submatrix checks for transition rewards in MDPs. Extended a test for the ExplicitModelAdapter a bit.
Former-commit-id: 105efc5342
11 years ago
dehnert
c82efc1f41
Minor fix.
Former-commit-id: 934f0d0f06
11 years ago
dehnert
f7293ee4a9
Merge branch 'master' into MinimalCommandCounterexample
Conflicts:
src/counterexamples/MinimalLabelSetGenerator.h
src/storm.cpp
Former-commit-id: 75f9e8adef
11 years ago
dehnert
129fd296d6
Several fixes. MinimalLabelSetGenerator can now treat labeled values.
Former-commit-id: 0fc3d8ead3
11 years ago
dehnert
a99bdf1b17
Switched to more elegant solution to query initial states of a model.
Former-commit-id: 9a5c90c5d5
11 years ago
dehnert
84f1b192b4
Added globally unique indexes to updates in IR. Finalized support for labeled values in ExplicitModelAdapter. Modified tests to comply with the new usage of ExplicitModelAdapter.
Former-commit-id: f6d5a33d6d
11 years ago
dehnert
61e12601ed
Further step towards refactored ExplicitModelAdapter.
Former-commit-id: 8abc07a366
11 years ago
dehnert
a08a403eec
Ongoing refactoring work on ExplicitModelAdapter.
Former-commit-id: 1212f84aad
11 years ago
dehnert
e2b0c4f1aa
Started refactoring ExplicitModelAdapter to finally make it nice.
Former-commit-id: 6df7e5d9fa
11 years ago
dehnert
fdfb8ecc97
Minor fixes.
Former-commit-id: f2298d312a
11 years ago
dehnert
f39fb24f65
Removed pointers from Model Checker Interface (and callback methods in formulas). From now on, the results are returned in form of an object. Because of the existing move semantics for the types in question, this does not come at a performance penalty.
Former-commit-id: 5befdebd92
11 years ago
dehnert
2aa8d11101
Removed unnecessary option. Fixed performance tests.
Former-commit-id: 183c546953
11 years ago
dehnert
d8e85ec071
Removed guessing of initial scheduler as this was just an idea and not meant to be in master at this point.
Former-commit-id: 1b74c9936d
11 years ago
PBerger
11cc7fc6bc
Introduced a new Object called InternalOptionMemento to handle required settings for tests which auto-reset after the test is done
Refactored many constants to be of type ull where required
Edited all tests that used the set() function of the Settings to make use of the new InternalOptionMemento
Former-commit-id: a400a36f69
11 years ago
dehnert
0f4e51e646
Changed notation to query option slightly.
Former-commit-id: 993a053306
11 years ago
PBerger
79c40126f3
Fixed a bug in the SparseMatrix.h where the multi threaded implementation would crash sometimes
Added a new definition to CMakeLists.txt for MSVC as to undefine the MIN/MAX macros
Former-commit-id: 5a3d12e920
11 years ago
PBerger
c242dcbd97
Refactored CMakeLists.txt for better editing and overview
Refactored all Defines for Gurobi, TBB, etc into the storm-config file
Fixed a missing cast int SymbolicModelAdapter.h
Fixed changed iterator structures in SparseMatrix.h
Fixed bugs in CuddUtility.cpp where a 64bit shift was executed on a 32bit literal (1 should be 1ull)
Fixed a Type Error in graph.h
Former-commit-id: 797b4da2eb
11 years ago
dehnert
b546118c98
Gurobi output now only gets printed to standard out and logfile if --debug has been set.
Former-commit-id: 4cd300ec5e
11 years ago
dehnert
5d76fd5ba0
Disabled model output to file.
Former-commit-id: be3eb00875
11 years ago
dehnert
014be3cb39
MinimalLabelSetGenerator can now handle multiple initial states properly.
Former-commit-id: 86f73a68a7
11 years ago
PBerger
6fca000233
Removed defines.hxx from source tree
Added a new include path for storm as to include the generated out-of-source defines.hxx
Former-commit-id: 1a75f61da0
11 years ago
dehnert
6e41ee360d
Fixes to several problems with gcc.
Former-commit-id: f7908fdc6f
11 years ago
dehnert
e4e4c783da
Readded defines.hxx.
Former-commit-id: 5a31bcbb50
11 years ago
dehnert
1934bdd801
Disabled MinimalLabelSetGenerator test code in storm.cpp and fixed minor issue in ExplicitModelAdapter that treated constant strings incorrectly.
Former-commit-id: 11a31be820
11 years ago
dehnert
6125898e69
Merge branch 'MinimalCommandCounterexample' of https://sselab.de/lab9/private/git/storm into MinimalCommandCounterexample
Former-commit-id: df67ab63b5
11 years ago
PBerger
cb1c3965ba
Removed a wrong and unnecessary validation function from ExplicitModelAdapter.cpp
Former-commit-id: 9f1aeaf27c
11 years ago
PBerger
8d59e1c91e
Removed an config input file from the repo
Former-commit-id: 5019b5d84c
11 years ago
dehnert
b782288833
Merge branch 'MinimalCommandCounterexample' of https://sselab.de/lab9/private/git/storm into MinimalCommandCounterexample
Former-commit-id: bb699dd856
11 years ago
dehnert
0ac3efb082
Finished merge of CMakeLists.txt
Former-commit-id: c4f903e8c5
11 years ago
PBerger
4b3d4a7c11
Removed buggy logging in setup-routines
Former-commit-id: ba57953947
11 years ago
dehnert
fe3012f69d
Merge branch 'master' into MinimalCommandCounterexample
Conflicts:
CMakeLists.txt
resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt
Former-commit-id: 890b34ca8f
11 years ago
dehnert
f1c800f382
Minor fixes to MinimalLabelSetGenerator and AbstractModel.
Former-commit-id: 83ee7ae262
11 years ago
PBerger
ef850b213b
Added the option -ftemplate-depth=1024 for Clang
Former-commit-id: 063b420dea
11 years ago
PBerger
3a38abec6f
Removed unnecessary names for unused variables in the ExplicitModelAdapter.cpp
Former-commit-id: bed4f234af
11 years ago
PBerger
f7a7ea8383
Fixed the StringValidator for the constants option
Fixed a bug in the MinimalLabelSetGenerator.h where a non static variable was initialized
Added the new constants option in storm.cpp
Former-commit-id: e73e69b1ce
11 years ago
PBerger
ef8008d6e3
Merge branch 'MinimalCommandCounterexample' of https://sselab.de/lab9/private/git/storm into MinimalCommandCounterexample
Former-commit-id: a67a69fe7d
11 years ago
PBerger
b79fde1a42
Added a definition for GTest to build with MSVC on Windows
Former-commit-id: 5ccb773886
11 years ago
PBerger
59ca0373a5
Removed a template specialization for std::less with the SafraTree.
Former-commit-id: 88209e9fee
11 years ago
PBerger
8e93238e18
Fixed a stray void* to char* conversion (still trying to please Clang)
Former-commit-id: eb1514ffb1
11 years ago
PBerger
08a30c6aad
Patched types for the strange version of qsort included in CUDD
Former-commit-id: e9d69d3514
11 years ago