dehnert
|
1fb943b658
|
moved some internal structs from model builder to their own files to make them reusable
Former-commit-id: a354059fe8
|
9 years ago |
dehnert
|
ca354cffe4
|
moved preprocessing of PRISM program to utility to make it accessible from learning-based model checker
Former-commit-id: 704dde9ec5
|
9 years ago |
dehnert
|
2df485a144
|
Merge branch 'future' into learning_engine
Former-commit-id: b9bceaa40d
|
9 years ago |
dehnert
|
dae55eeb29
|
fixed some bugs and enabled markov automaton model checking from cli
Former-commit-id: 91b689d817
|
9 years ago |
dehnert
|
aac9ba469b
|
Merge branch 'future' into learning_engine
Former-commit-id: 801a989353
|
9 years ago |
dehnert
|
7dee6d3da2
|
started on learning-based MDP model checking
Former-commit-id: 9a901e619b
|
9 years ago |
dehnert
|
bb7d8ca3c5
|
added learning as new engine selection in options
Former-commit-id: e00c7ad75d
|
9 years ago |
dehnert
|
adb42b3ac0
|
fixed minor things related to merge
Former-commit-id: f428c2808b
|
9 years ago |
dehnert
|
e23a7f854a
|
Merge branch 'future' into next_state_generators
Former-commit-id: bcdf6cb4b3
|
9 years ago |
dehnert
|
4a19d81133
|
fixed a few bugs
Former-commit-id: 70d408e653
|
9 years ago |
dehnert
|
6a99ab9ef9
|
expectation/variance now handled in formula parser
Former-commit-id: 9dbe09411c
|
9 years ago |
dehnert
|
51402ec853
|
removed measure type and only added measure type to reward/time operators
Former-commit-id: 16e19fe349
|
9 years ago |
dehnert
|
f86bfdd46f
|
Merge branch 'future' into variance_properties
Former-commit-id: 74258afddd
|
9 years ago |
dehnert
|
39acf24448
|
fix for weak bisimulation on CTMCs
Former-commit-id: 4eee2e0997
|
9 years ago |
dehnert
|
016ab53f42
|
making the logic formulas better
Former-commit-id: bd5dd26c51
|
9 years ago |
dehnert
|
5e1e5b55a1
|
renamed expected time formulas to time formulas
Former-commit-id: 50a11fe446
|
9 years ago |
dehnert
|
9cda76c675
|
Merge branch 'future' into variance_properties
Former-commit-id: 13fe1e8531
|
9 years ago |
TimQu
|
6e8602413e
|
ModelInstantiator + test
Former-commit-id: f3c9980067
|
9 years ago |
TimQu
|
69c5ba604e
|
Helper functions for parametric stuff
Former-commit-id: 288e4de3da
|
9 years ago |
TimQu
|
a3aededd3a
|
public access to model ingredients: RewardModel and exitRates
Former-commit-id: b8dbe8576e
|
9 years ago |
dehnert
|
45e59848a9
|
first steps
Former-commit-id: 12d930813b1b2856104f9ac32f1b9b1af09a251e
|
9 years ago |
dehnert
|
f54c2fb8e7
|
tests passing again
Former-commit-id: 8e3311f4c7afd7dfc456e22ad7998b929aee76ed
|
9 years ago |
dehnert
|
a40d12f915
|
made getRowGroup more consistent and fixed some introduced bugs
Former-commit-id: 99b6c0e3a5b5d263c185fbd4bdb08d435c5b688b
|
9 years ago |
dehnert
|
0b98412bb4
|
further work on making row-grouping optional
Former-commit-id: bae568660f238424524b14694d39929165801aa5
|
9 years ago |
TimQu
|
f285858e28
|
added required includes
Former-commit-id: c523950b43c43d91ae19f3258683c53b7e19f650
|
9 years ago |
dehnert
|
f81ce1cac1
|
started making row grouping optional
Former-commit-id: b90ae91e754087bc55f35993b66713ab60edc7e5
|
9 years ago |
dehnert
|
1f5439e270
|
added state labeling generator interface
Former-commit-id: eb7668741fa1561dbb2bd3c043a7b4b5674327fe
|
9 years ago |
dehnert
|
1dd2a5c808
|
Merge branch 'future' into next_state_generators
Former-commit-id: 93bfabf944bc6199848bd070eee52a141e6faec0
|
9 years ago |
dehnert
|
c45812c66a
|
made bfs the default exploration order again
Former-commit-id: 6476c48a6798c7a48343da7626e27d28fe57ace5
|
9 years ago |
dehnert
|
ffe63ea95d
|
made dfs as exploration order available
Former-commit-id: 46ea31af78b5819690fcc0a47ef9c1565c109c2b
|
9 years ago |
dehnert
|
55fd1b66c3
|
introducing exploration orders to explicit builder
Former-commit-id: a56620eac2c37abbda99a16ff2dc880813e2b185
|
9 years ago |
dehnert
|
0dfdfe7db8
|
using flat_map in model building instead of unordered_map
Former-commit-id: ff895d2bcc95582afafdaae0760df92ea801693d
|
9 years ago |
dehnert
|
fff7b2d5db
|
fixed an allocation issue, performance is now roughly the same as before but memory consumption is reduced
Former-commit-id: ff4480497502ea159c87a8de216f469683ebf2ea
|
9 years ago |
dehnert
|
fad28df7d6
|
first working version of next-state generator for PRISM models
Former-commit-id: 548a725e254bcbb924de20f37f24c93fcd916c9b
|
9 years ago |
Mavo
|
e9b4f06972
|
Better assertions in BitVector
Former-commit-id: 7ee6b34ba5bced25fca9e1702e32a451e69f7d30
|
9 years ago |
sjunges
|
4a1f7468f5
|
param result file now has a semicolon between parameters
Former-commit-id: f9896d0d043550144adc92a811dc8408d708014d
|
9 years ago |
dehnert
|
9eec5b140c
|
refactoring of model builder
Former-commit-id: f049f5a5bf4d759caae6a037cc12ca5ae56bfda0
|
9 years ago |
sjunges
|
c007c8e699
|
add sylvan to the resources target
Former-commit-id: 70e3c16f555d8a60ea6f2f6c91fcc91692175095
|
9 years ago |
dehnert
|
9506f4f420
|
Merge branch 'future' into next_state_generators
Former-commit-id: a34608d2a0ca8435f6c5ae2035719d74762795fb
|
9 years ago |
sjunges
|
fde7b71933
|
Nice printing when no logging framework is enabled
Former-commit-id: 783fe7eea12722d4abc1b0187353ddef50ed84e7
|
9 years ago |
sjunges
|
8c2cb4887f
|
Cmake option to disable debug and trace outputs
Former-commit-id: 9758862579554eb3f83af62c09cfef5e4dbcd06c
|
9 years ago |
sjunges
|
6818c6dc0d
|
Fixed tests when no log4plus is available.
Former-commit-id: f1ae81376c79043b32e8a05f2a9b5c1a1bed4227
|
9 years ago |
sjunges
|
fcd98793ee
|
fixed supp for log4cplus
Former-commit-id: 7e0b2c449fa78bf216a8e581165baf034484b4a3
|
9 years ago |
sjunges
|
cf986311ad
|
loglevel can be set now and all logging macros support streaming
Former-commit-id: c8c32b43e64da8e266c471f5d50ae8a3e6495397
|
9 years ago |
sjunges
|
abac11ab50
|
sylvan build stuff in 3rd party folder now
Former-commit-id: 3ea163dfeda863332440ff3ba19ae3d6747ed60e
|
9 years ago |
sjunges
|
e0379b9c50
|
Log CUDD build process
Former-commit-id: daf41bb2654b99a08699160937c6218cb18bce8e
|
9 years ago |
sjunges
|
e0980de0ba
|
first version of storm without log4cplus as a dependency
Former-commit-id: 5aa64fabd71b7f6a02b46de3336d1f1b55de74d6
|
9 years ago |
dehnert
|
a75e0f5323
|
more work wrt cleaner model exploration
Former-commit-id: f24d618bdf08e22aa28f7f6baf045b56bc98e9d8
|
9 years ago |
dehnert
|
08bed36579
|
fixed an issue in performance tests and renamed all remaining LOG4CPLUS macro invocations to that of storm
Former-commit-id: 8536943978e7313a9f9834d3f790973b7868e204
|
9 years ago |
dehnert
|
865345c7bf
|
a little morning code
Former-commit-id: 9cb63427c66ed48e3454d1e221a4a02cf60e5514
|
9 years ago |