sjunges
7 years ago
442 changed files with 45807 additions and 31641 deletions
-
2.gitignore
-
398.travis.yml
-
11CHANGELOG.md
-
92CMakeLists.txt
-
4README.md
-
4resources/3rdparty/CMakeLists.txt
-
3190resources/3rdparty/cudd-3.0.0/Makefile.in
-
1256resources/3rdparty/cudd-3.0.0/aclocal.m4
-
19890resources/3rdparty/cudd-3.0.0/configure
-
15resources/cmake/find_modules/FindGurobi.cmake
-
4resources/cmake/find_modules/FindZ3.cmake
-
52resources/cmake/macros/GetGitRevisionDescription.cmake
-
13resources/cmake/macros/GetGitRevisionDescription.cmake.in
-
20resources/cmake/macros/export.cmake
-
11resources/cmake/stormConfigVersion.cmake.in
-
554resources/examples/testfiles/ctmc/cluster2.drn
-
4resources/examples/testfiles/dft/and.dft
-
8resources/examples/testfiles/dft/fdep.dft
-
5resources/examples/testfiles/dft/fdep2.dft
-
5resources/examples/testfiles/dft/fdep3.dft
-
7resources/examples/testfiles/dft/fdep4.dft
-
7resources/examples/testfiles/dft/fdep5.dft
-
4resources/examples/testfiles/dft/or.dft
-
4resources/examples/testfiles/dft/pand.dft
-
12resources/examples/testfiles/dft/pdep.dft
-
9resources/examples/testfiles/dft/pdep2.dft
-
5resources/examples/testfiles/dft/pdep3.dft
-
7resources/examples/testfiles/dft/pdep4.dft
-
5resources/examples/testfiles/dft/por.dft
-
5resources/examples/testfiles/dft/seq.dft
-
6resources/examples/testfiles/dft/seq2.dft
-
6resources/examples/testfiles/dft/seq3.dft
-
7resources/examples/testfiles/dft/seq4.dft
-
9resources/examples/testfiles/dft/seq5.dft
-
5resources/examples/testfiles/dft/spare.dft
-
8resources/examples/testfiles/dft/spare2.dft
-
10resources/examples/testfiles/dft/spare3.dft
-
9resources/examples/testfiles/dft/spare4.dft
-
9resources/examples/testfiles/dft/spare5.dft
-
7resources/examples/testfiles/dft/spare6.dft
-
5resources/examples/testfiles/dft/spare7.dft
-
7resources/examples/testfiles/dft/spare8.dft
-
5resources/examples/testfiles/dft/voting.dft
-
5resources/examples/testfiles/dft/voting2.dft
-
5resources/examples/testfiles/dft/voting3.dft
-
6resources/examples/testfiles/dft/voting4.dft
-
32337resources/examples/testfiles/dtmc/crowds-5-5.drn
-
71resources/examples/testfiles/ma/jobscheduler.drn
-
12resources/examples/testfiles/mdp/prism-mec-example1.nm
-
13resources/examples/testfiles/mdp/prism-mec-example2.nm
-
2resources/examples/testfiles/mdp/two_dice.drn
-
2src/storm-cli-utilities/CMakeLists.txt
-
27src/storm-cli-utilities/cli.cpp
-
7src/storm-cli-utilities/cli.h
-
108src/storm-cli-utilities/model-handling.h
-
2src/storm-dft-cli/CMakeLists.txt
-
201src/storm-dft-cli/storm-dft.cpp
-
2src/storm-dft/CMakeLists.txt
-
67src/storm-dft/api/storm-dft.cpp
-
117src/storm-dft/api/storm-dft.h
-
118src/storm-dft/builder/DFTBuilder.cpp
-
50src/storm-dft/builder/DFTBuilder.h
-
8src/storm-dft/modelchecker/dft/DFTASFChecker.h
-
58src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
-
7src/storm-dft/modelchecker/dft/DFTModelChecker.h
-
279src/storm-dft/parser/DFTGalileoParser.cpp
-
58src/storm-dft/parser/DFTGalileoParser.h
-
4src/storm-dft/parser/DFTJsonParser.h
-
10src/storm-dft/settings/DftSettings.cpp
-
9src/storm-dft/settings/modules/DftIOSettings.cpp
-
10src/storm-dft/settings/modules/DftIOSettings.h
-
2src/storm-dft/storage/BucketPriorityQueue.cpp
-
72src/storm-dft/storage/dft/DFT.cpp
-
16src/storm-dft/storage/dft/DFT.h
-
826src/storm-dft/transformations/DftToGspnTransformator.cpp
-
219src/storm-dft/transformations/DftToGspnTransformator.h
-
2src/storm-gspn-cli/CMakeLists.txt
-
28src/storm-gspn-cli/storm-gspn.cpp
-
2src/storm-gspn/CMakeLists.txt
-
61src/storm-gspn/api/storm-gspn.cpp
-
17src/storm-gspn/api/storm-gspn.h
-
2src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
-
5src/storm-gspn/parser/PnmlParser.cpp
-
11src/storm-gspn/settings/modules/GSPNExportSettings.cpp
-
8src/storm-gspn/settings/modules/GSPNExportSettings.h
-
76src/storm-gspn/storage/gspn/GSPN.cpp
-
14src/storm-gspn/storage/gspn/GSPN.h
-
2src/storm-gspn/storage/gspn/GspnBuilder.cpp
-
2src/storm-gspn/storage/gspn/GspnBuilder.h
-
203src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
-
71src/storm-gspn/storage/gspn/GspnJsonExporter.h
-
3src/storm-gspn/storage/gspn/Place.cpp
-
4src/storm-gspn/storage/gspn/Place.h
-
62src/storm-gspn/storm-gspn.h
-
2src/storm-pars-cli/CMakeLists.txt
-
2src/storm-pars/CMakeLists.txt
-
92src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
-
12src/storm-pars/settings/ParsSettings.cpp
-
2src/storm-pgcl-cli/CMakeLists.txt
-
2src/storm-pgcl/CMakeLists.txt
3190
resources/3rdparty/cudd-3.0.0/Makefile.in
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
1256
resources/3rdparty/cudd-3.0.0/aclocal.m4
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
19890
resources/3rdparty/cudd-3.0.0/configure
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,11 @@ |
|||
set(PACKAGE_VERSION "@storm_VERSION@") |
|||
|
|||
# Check whether the requested PACKAGE_FIND_VERSION is compatible |
|||
if("${PACKAGE_VERSION}" VERSION_LESS "${PACKAGE_FIND_VERSION}") |
|||
set(PACKAGE_VERSION_COMPATIBLE FALSE) |
|||
else() |
|||
set(PACKAGE_VERSION_COMPATIBLE TRUE) |
|||
if ("${PACKAGE_VERSION}" VERSION_EQUAL "${PACKAGE_FIND_VERSION}") |
|||
set(PACKAGE_VERSION_EXACT TRUE) |
|||
endif() |
|||
endif() |
|||
554
resources/examples/testfiles/ctmc/cluster2.drn
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,4 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -0,0 +1,8 @@ |
|||
toplevel "System"; |
|||
"System" or "Power" "Machine"; |
|||
"Power" fdep "B_Power" "P" "B"; |
|||
"Machine" or "P" "B"; |
|||
|
|||
"B_Power" lambda=0.5 dorm=0; |
|||
"P" lambda=0.5 dorm=0; |
|||
"B" lambda=0.5 dorm=0.5; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"F" fdep "B" "C"; |
|||
"B" lambda=0.5 dorm=0; |
|||
"C" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "F"; |
|||
"F" fdep "B" "C"; |
|||
"B" lambda=0.4 dorm=0; |
|||
"C" lambda=0.8 dorm=0; |
|||
@ -0,0 +1,7 @@ |
|||
toplevel "A"; |
|||
"A" or "F" "B"; |
|||
"F" fdep "E" "C" "D"; |
|||
"B" wsp "C" "D"; |
|||
"C" lambda=1 dorm=0; |
|||
"D" lambda=1 dorm=0.5; |
|||
"E" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,7 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "D" "E"; |
|||
"F" fdep "B" "C" "D"; |
|||
"B" lambda=0.5 dorm=0; |
|||
"C" lambda=0.5 dorm=0; |
|||
"D" lambda=0.5 dorm=0; |
|||
"E" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,4 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -0,0 +1,4 @@ |
|||
toplevel "A"; |
|||
"A" pand "B" "C"; |
|||
"B" lambda=0.4 dorm=0.3; |
|||
"C" lambda=0.2 dorm=0.3; |
|||
@ -0,0 +1,12 @@ |
|||
// From Junges2015 |
|||
// Example 3.19 |
|||
|
|||
toplevel "SF"; |
|||
"SF" or "A" "B" "PDEP"; |
|||
"A" pand "S" "MA"; |
|||
"B" and "MA" "MB"; |
|||
"PDEP" pdep=0.2 "MA" "S"; |
|||
|
|||
"S" lambda=0.5 dorm=0; |
|||
"MA" lambda=0.5 dorm=0; |
|||
"MB" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,9 @@ |
|||
toplevel "SF"; |
|||
"SF" or "A" "B" "PDEP"; |
|||
"A" pand "S" "MA"; |
|||
"B" and "MA" "MB"; |
|||
"PDEP" pdep=0.2 "MA" "S" "MB"; |
|||
|
|||
"S" lambda=0.5 dorm=0; |
|||
"MA" lambda=0.5 dorm=0; |
|||
"MB" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "F"; |
|||
"F" pdep=0.3 "B" "C"; |
|||
"B" lambda=0.4 dorm=0; |
|||
"C" lambda=0.8 dorm=0; |
|||
@ -0,0 +1,7 @@ |
|||
toplevel "SF"; |
|||
"SF" pand "S" "A" "B"; |
|||
"PDEP" pdep=0.2 "S" "A" "B"; |
|||
|
|||
"S" lambda=0.5 dorm=0; |
|||
"A" lambda=0.5 dorm=0; |
|||
"B" lambda=0.5 dorm=0; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" por "B" "C" "D"; |
|||
"B" lambda=0.4 dorm=0.0; |
|||
"C" lambda=0.2 dorm=0.0; |
|||
"D" lambda=0.2 dorm=0.0; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"X" seq "B" "C"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
@ -0,0 +1,6 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C" "D"; |
|||
"X" seq "B" "C" "D"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
"D" lambda=0.5 dorm=0.3; |
|||
@ -0,0 +1,6 @@ |
|||
toplevel "A"; |
|||
"A" and "C" "D"; |
|||
"X" seq "B" "C" "D"; |
|||
"B" lambda=0.5 dorm=0.3; |
|||
"C" lambda=0.5 dorm=0.3; |
|||
"D" lambda=0.5 dorm=0.3; |
|||
@ -0,0 +1,7 @@ |
|||
toplevel "A"; |
|||
"A" and "T1" "B3"; |
|||
"T1" or "B1" "B2"; |
|||
"X" seq "B1" "B2" "B3"; |
|||
"B1" lambda=0.5 dorm=0.3; |
|||
"B2" lambda=0.5 dorm=0.3; |
|||
"B3" lambda=0.5 dorm=0.3; |
|||
@ -0,0 +1,9 @@ |
|||
toplevel "A"; |
|||
"A" and "T1" "T2"; |
|||
"T1" pand "B1" "B2"; |
|||
"T2" pand "B3" "B4"; |
|||
"X" seq "B4" "B3"; |
|||
"B1" lambda=0.7 dorm=0.3; |
|||
"B2" lambda=0.5 dorm=0.3; |
|||
"B3" lambda=0.5 dorm=0.3; |
|||
"B4" lambda=0.7 dorm=0.3; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "M"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -0,0 +1,8 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C"; |
|||
"B" wsp "I" "J"; |
|||
"C" wsp "M" "J"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -0,0 +1,10 @@ |
|||
toplevel "A"; |
|||
"A" or "B" "C" "D"; |
|||
"B" wsp "I" "M"; |
|||
"C" wsp "J" "M"; |
|||
"D" wsp "K" "M"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -0,0 +1,9 @@ |
|||
toplevel "A"; |
|||
"A" and "B" "C"; |
|||
"B" wsp "I" "J" "K"; |
|||
"C" wsp "M" "J"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
"M" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -0,0 +1,9 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "B"; |
|||
"B" or "C" "J"; |
|||
"C" or "K" "L"; |
|||
"I" lambda=0.5 dorm=0; |
|||
"J" lambda=0.5 dorm=0; |
|||
"K" lambda=0.5 dorm=0; |
|||
"L" lambda=0.5 dorm=0; |
|||
|
|||
@ -0,0 +1,7 @@ |
|||
toplevel "A"; |
|||
"A" or "I" "B"; |
|||
"B" wsp "J" "M"; |
|||
"I" lambda=0.5 dorm=0.5; |
|||
"J" lambda=0.5 dorm=0.5; |
|||
"M" lambda=0.5 dorm=0.5; |
|||
|
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" wsp "K" "J" "I"; |
|||
"I" lambda=0.5 dorm=0.5; |
|||
"J" lambda=1 dorm=0.5; |
|||
"K" lambda=0.5 dorm=0.5; |
|||
@ -0,0 +1,7 @@ |
|||
toplevel "A"; |
|||
"A" wsp "I" "B"; |
|||
"B" wsp "J" "K"; |
|||
"I" lambda=0.5 dorm=0.3; |
|||
"J" lambda=0.5 dorm=0.3; |
|||
"K" lambda=0.5 dorm=0.3; |
|||
|
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" 1of3 "B" "C" "D"; |
|||
"B" lambda=0.1 dorm=0; |
|||
"C" lambda=0.2 dorm=0; |
|||
"D" lambda=0.3 dorm=0; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" 1of3 "B" "C" "D"; |
|||
"B" lambda=0.3 dorm=0; |
|||
"C" lambda=0.4 dorm=0; |
|||
"D" lambda=1 dorm=0; |
|||
@ -0,0 +1,5 @@ |
|||
toplevel "A"; |
|||
"A" 2of3 "B" "C" "D"; |
|||
"B" lambda=0.3 dorm=0; |
|||
"C" lambda=0.4 dorm=0; |
|||
"D" lambda=1 dorm=0; |
|||
@ -0,0 +1,6 @@ |
|||
toplevel "A"; |
|||
"A" 2of3 "B" "C" "D"; |
|||
"D" or "E"; |
|||
"B" lambda=1 dorm=0.0; |
|||
"C" lambda=1 dorm=0.0; |
|||
"E" lambda=1 dorm=0.0; |
|||
32337
resources/examples/testfiles/dtmc/crowds-5-5.drn
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,71 @@ |
|||
// Exported by storm |
|||
// Original model type: Markov Automaton |
|||
@type: Markov Automaton |
|||
@parameters |
|||
|
|||
@reward_models |
|||
avg_waiting_time |
|||
@nr_states |
|||
17 |
|||
@model |
|||
state 0 !0 [1] init |
|||
action 0 [0] |
|||
1 : 1 |
|||
action 1 [0] |
|||
2 : 1 |
|||
action 2 [0] |
|||
3 : 1 |
|||
state 1 !3 [1] |
|||
action 0 [0] |
|||
4 : 0.333333 |
|||
5 : 0.666667 |
|||
state 2 !4 [1] |
|||
action 0 [0] |
|||
4 : 0.25 |
|||
6 : 0.75 |
|||
state 3 !5 [1] |
|||
action 0 [0] |
|||
5 : 0.4 |
|||
6 : 0.6 |
|||
state 4 !0 [0.666667] one_job_finished slowest_before_fastest |
|||
action 0 [0] |
|||
7 : 1 |
|||
state 5 !0 [0.666667] one_job_finished |
|||
action 0 [0] |
|||
8 : 1 |
|||
state 6 !0 [0.666667] one_job_finished |
|||
action 0 [0] |
|||
9 : 1 |
|||
state 7 !5 [0.666667] one_job_finished slowest_before_fastest |
|||
action 0 [0] |
|||
10 : 0.4 |
|||
11 : 0.6 |
|||
state 8 !4 [0.666667] one_job_finished |
|||
action 0 [0] |
|||
10 : 0.25 |
|||
12 : 0.75 |
|||
state 9 !3 [0.666667] one_job_finished |
|||
action 0 [0] |
|||
11 : 0.333333 |
|||
12 : 0.666667 |
|||
state 10 !0 [0.333333] half_of_jobs_finished slowest_before_fastest |
|||
action 0 [0] |
|||
13 : 1 |
|||
state 11 !0 [0.333333] half_of_jobs_finished |
|||
action 0 [0] |
|||
14 : 1 |
|||
state 12 !0 [0.333333] half_of_jobs_finished |
|||
action 0 [0] |
|||
15 : 1 |
|||
state 13 !3 [0.333333] half_of_jobs_finished slowest_before_fastest |
|||
action 0 [0] |
|||
16 : 1 |
|||
state 14 !2 [0.333333] half_of_jobs_finished |
|||
action 0 [0] |
|||
16 : 1 |
|||
state 15 !1 [0.333333] half_of_jobs_finished |
|||
action 0 [0] |
|||
16 : 1 |
|||
state 16 !1 [0] all_jobs_finished deadlock |
|||
action 0 [0] |
|||
16 : 1 |
|||
@ -0,0 +1,12 @@ |
|||
mdp |
|||
|
|||
module test |
|||
|
|||
x : [0..2]; |
|||
|
|||
[] x=0 -> true; |
|||
[] x=0 -> 0.5 : (x'=1) + 0.5: (x'=2); |
|||
[] x=1 -> (x'=0); |
|||
[] x=2 -> true; |
|||
|
|||
endmodule |
|||
@ -0,0 +1,13 @@ |
|||
mdp |
|||
|
|||
module test |
|||
|
|||
x : [0..2]; |
|||
|
|||
[] x=0 -> true; |
|||
[] x=0 -> 0.5 : (x'=1) + 0.5: (x'=1); |
|||
[] x=0 -> (x'=2); |
|||
[] x=1 -> (x'=0); |
|||
[] x=2 -> true; |
|||
|
|||
endmodule |
|||
@ -0,0 +1,67 @@ |
|||
#include "storm-dft/api/storm-dft.h"
|
|||
|
|||
namespace storm { |
|||
namespace api { |
|||
|
|||
template<> |
|||
void exportDFTToJson(storm::storage::DFT<double> const& dft, std::string const& file) { |
|||
storm::storage::DftJsonExporter<double>::toFile(dft, file); |
|||
} |
|||
|
|||
template<> |
|||
void exportDFTToJson(storm::storage::DFT<storm::RationalFunction> const& dft, std::string const& file) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to JSON not supported for this data type."); |
|||
} |
|||
|
|||
template<> |
|||
void exportDFTToSMT(storm::storage::DFT<double> const& dft, std::string const& file) { |
|||
storm::modelchecker::DFTASFChecker asfChecker(dft); |
|||
asfChecker.convert(); |
|||
asfChecker.toFile(file); |
|||
} |
|||
|
|||
template<> |
|||
void exportDFTToSMT(storm::storage::DFT<storm::RationalFunction> const& dft, std::string const& file) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); |
|||
} |
|||
|
|||
template<> |
|||
void transformToGSPN(storm::storage::DFT<double> const& dft) { |
|||
// Transform to GSPN
|
|||
storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft); |
|||
bool smart = true; |
|||
gspnTransformator.transform(smart); |
|||
storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); |
|||
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); |
|||
|
|||
storm::api::handleGSPNExportSettings(*gspn); |
|||
|
|||
std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager(); |
|||
storm::builder::JaniGSPNBuilder builder(*gspn); |
|||
storm::jani::Model* model = builder.build(); |
|||
storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); |
|||
|
|||
storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); |
|||
auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression); |
|||
auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); |
|||
auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula); |
|||
|
|||
auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time); |
|||
auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation); |
|||
|
|||
storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>(); |
|||
if (janiSettings.isJaniFileSet()) { |
|||
storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename()); |
|||
} |
|||
|
|||
delete model; |
|||
delete gspn; |
|||
} |
|||
|
|||
template<> |
|||
void transformToGSPN(storm::storage::DFT<storm::RationalFunction> const& dft) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,117 @@ |
|||
#pragma once |
|||
|
|||
#include <type_traits> |
|||
|
|||
#include "storm-dft/parser/DFTGalileoParser.h" |
|||
#include "storm-dft/parser/DFTJsonParser.h" |
|||
#include "storm-dft/storage/dft/DftJsonExporter.h" |
|||
|
|||
#include "storm-dft/modelchecker/dft/DFTModelChecker.h" |
|||
#include "storm-dft/modelchecker/dft/DFTASFChecker.h" |
|||
|
|||
#include "storm-dft/transformations/DftToGspnTransformator.h" |
|||
#include "storm-gspn/api/storm-gspn.h" |
|||
|
|||
namespace storm { |
|||
namespace api { |
|||
|
|||
/*! |
|||
* Load DFT from Galileo file. |
|||
* |
|||
* @param file File containing DFT description in Galileo format. |
|||
* |
|||
* @return DFT. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileo(std::string const& file) { |
|||
return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file)); |
|||
} |
|||
|
|||
/*! |
|||
* Load DFT from JSON file. |
|||
* |
|||
* @param file File containing DFT description in JSON format. |
|||
* |
|||
* @return DFT. |
|||
*/ |
|||
template<typename ValueType> |
|||
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJson(std::string const& file) { |
|||
storm::parser::DFTJsonParser<ValueType> parser; |
|||
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(file)); |
|||
} |
|||
|
|||
/*! |
|||
* Analyse the given DFT according to the given properties. |
|||
* First the Markov model is built from the DFT and then this model is checked against the given properties. |
|||
* |
|||
* @param dft DFT. |
|||
* @param properties PCTL formulas capturing the properties to check. |
|||
* @param symred Flag whether symmetry reduction should be used. |
|||
* @param allowModularisation Flag whether modularisation should be applied if possible. |
|||
* @param enableDC Flag whether Don't Care propagation should be used. |
|||
* |
|||
* @return Result. |
|||
*/ |
|||
template <typename ValueType> |
|||
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) { |
|||
storm::modelchecker::DFTModelChecker<ValueType> modelChecker; |
|||
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); |
|||
if (printOutput) { |
|||
modelChecker.printTimings(); |
|||
modelChecker.printResults(); |
|||
} |
|||
return results; |
|||
} |
|||
|
|||
/*! |
|||
* Approximate the analysis result of the given DFT according to the given properties. |
|||
* First the Markov model is built from the DFT and then this model is checked against the given properties. |
|||
* |
|||
* @param dft DFT. |
|||
* @param properties PCTL formulas capturing the properties to check. |
|||
* @param symred Flag whether symmetry reduction should be used. |
|||
* @param allowModularisation Flag whether modularisation should be applied if possible. |
|||
* @param enableDC Flag whether Don't Care propagation should be used. |
|||
* @param approximationError Allowed approximation error. |
|||
* |
|||
* @return Result. |
|||
*/ |
|||
template <typename ValueType> |
|||
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { |
|||
storm::modelchecker::DFTModelChecker<ValueType> modelChecker; |
|||
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); |
|||
if (printOutput) { |
|||
modelChecker.printTimings(); |
|||
modelChecker.printResults(); |
|||
} |
|||
return results; |
|||
} |
|||
|
|||
/*! |
|||
* Export DFT to JSON file. |
|||
* |
|||
* @param dft DFT. |
|||
* @param file File. |
|||
*/ |
|||
template<typename ValueType> |
|||
void exportDFTToJson(storm::storage::DFT<ValueType> const& dft, std::string const& file); |
|||
|
|||
/*! |
|||
* Export DFT to SMT encoding. |
|||
* |
|||
* @param dft DFT. |
|||
* @param file File. |
|||
*/ |
|||
template<typename ValueType> |
|||
void exportDFTToSMT(storm::storage::DFT<ValueType> const& dft, std::string const& file); |
|||
|
|||
/*! |
|||
* Transform DFT to GSPN. |
|||
* |
|||
* @param dft DFT. |
|||
*/ |
|||
template<typename ValueType> |
|||
void transformToGSPN(storm::storage::DFT<ValueType> const& dft); |
|||
|
|||
} |
|||
} |
|||
826
src/storm-dft/transformations/DftToGspnTransformator.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,61 @@ |
|||
#include "storm-gspn/api/storm-gspn.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/utility/file.h"
|
|||
#include "storm-gspn/settings/modules/GSPNExportSettings.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace api { |
|||
|
|||
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn) { |
|||
storm::builder::JaniGSPNBuilder builder(gspn); |
|||
return builder.build(); |
|||
} |
|||
|
|||
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) { |
|||
storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>(); |
|||
if (exportSettings.isWriteToDotSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToDotFilename(), fs); |
|||
gspn.writeDotToStream(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isWriteToPnproSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToPnproFilename(), fs); |
|||
gspn.toPnpro(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isWriteToPnmlSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToPnmlFilename(), fs); |
|||
gspn.toPnml(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isWriteToJsonSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToJsonFilename(), fs); |
|||
gspn.toJson(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isDisplayStatsSet()) { |
|||
std::cout << "============GSPN Statistics==============" << std::endl; |
|||
gspn.writeStatsToStream(std::cout); |
|||
std::cout << "=========================================" << std::endl; |
|||
} |
|||
|
|||
if (exportSettings.isWriteStatsToFileSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteStatsFilename(), fs); |
|||
gspn.writeStatsToStream(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,17 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/storage/jani/Model.h" |
|||
#include "storm-gspn/storage/gspn/GSPN.h" |
|||
#include "storm-gspn/builder/JaniGSPNBuilder.h" |
|||
|
|||
namespace storm { |
|||
namespace api { |
|||
|
|||
/** |
|||
* Builds JANI model from GSPN. |
|||
*/ |
|||
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn); |
|||
|
|||
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn); |
|||
} |
|||
} |
|||
@ -0,0 +1,203 @@ |
|||
#include "GspnJsonExporter.h"
|
|||
|
|||
#include "storm/exceptions/NotImplementedException.h"
|
|||
#include "storm/exceptions/FileIoException.h"
|
|||
|
|||
#include <algorithm>
|
|||
#include <string>
|
|||
|
|||
namespace storm { |
|||
namespace gspn { |
|||
|
|||
// Prevent some magic constants
|
|||
static constexpr const uint64_t scaleFactor = 50; |
|||
|
|||
|
|||
void GspnJsonExporter::toStream(storm::gspn::GSPN const& gspn, std::ostream& os) { |
|||
os << translate(gspn).dump(4) << std::endl; |
|||
} |
|||
|
|||
modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) { |
|||
modernjson::json jsonGspn; |
|||
|
|||
// Layouts
|
|||
std::map<uint64_t, LayoutInfo> placeLayout = gspn.getPlaceLayoutInfos(); |
|||
std::map<uint64_t, LayoutInfo> transitionLayout = gspn.getTransitionLayoutInfos(); |
|||
double tmpX = 0; |
|||
double tmpY = 10; |
|||
|
|||
// Export places
|
|||
for (const auto &place : gspn.getPlaces()) { |
|||
double x = tmpX; |
|||
double y = tmpY; |
|||
if (placeLayout.count(place.getID()) > 0) { |
|||
x = placeLayout.at(place.getID()).x; |
|||
y = placeLayout.at(place.getID()).y; |
|||
} |
|||
tmpX += 3; |
|||
modernjson::json jsonPlace = translatePlace(place, x, y); |
|||
jsonGspn.push_back(jsonPlace); |
|||
} |
|||
|
|||
// Export immediate transitions
|
|||
for (const auto &transition : gspn.getImmediateTransitions()) { |
|||
double x = tmpX; |
|||
double y = tmpY; |
|||
if (transitionLayout.count(transition.getID()) > 0) { |
|||
x = transitionLayout.at(transition.getID()).x; |
|||
y = transitionLayout.at(transition.getID()).y; |
|||
} |
|||
tmpX += 3; |
|||
modernjson::json jsonImmediateTransition = translateImmediateTransition(transition, x, y); |
|||
jsonGspn.push_back(jsonImmediateTransition); |
|||
} |
|||
|
|||
// Export timed transitions
|
|||
for (const auto &transition : gspn.getTimedTransitions()) { |
|||
double x = tmpX; |
|||
double y = tmpY; |
|||
if (transitionLayout.count(transition.getID()) > 0) { |
|||
x = transitionLayout.at(transition.getID()).x; |
|||
y = transitionLayout.at(transition.getID()).y; |
|||
} |
|||
tmpX += 3; |
|||
modernjson::json jsonTimedTransition = translateTimedTransition(transition, x, y); |
|||
jsonGspn.push_back(jsonTimedTransition); |
|||
} |
|||
|
|||
// Export arcs
|
|||
std::vector<storm::gspn::Place> places = gspn.getPlaces(); |
|||
// Export arcs for immediate transitions
|
|||
for (const auto &transition : gspn.getImmediateTransitions()) { |
|||
// Export input arcs
|
|||
for (auto const& entry : transition.getInputPlaces()) { |
|||
storm::gspn::Place place = places.at(entry.first); |
|||
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INPUT); |
|||
jsonGspn.push_back(jsonInputArc); |
|||
} |
|||
|
|||
// Export inhibitor arcs
|
|||
for (auto const& entry : transition.getInhibitionPlaces()) { |
|||
storm::gspn::Place place = places.at(entry.first); |
|||
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INHIBITOR); |
|||
jsonGspn.push_back(jsonInputArc); |
|||
} |
|||
|
|||
// Export output arcs
|
|||
for (auto const& entry : transition.getOutputPlaces()) { |
|||
storm::gspn::Place place = places.at(entry.first); |
|||
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::OUTPUT); |
|||
jsonGspn.push_back(jsonInputArc); |
|||
} |
|||
} |
|||
// Export arcs for timed transitions
|
|||
for (const auto &transition : gspn.getTimedTransitions()) { |
|||
// Export input arcs
|
|||
for (auto const& entry : transition.getInputPlaces()) { |
|||
storm::gspn::Place place = places.at(entry.first); |
|||
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INPUT); |
|||
jsonGspn.push_back(jsonInputArc); |
|||
} |
|||
|
|||
// Export inhibitor arcs
|
|||
for (auto const& entry : transition.getInhibitionPlaces()) { |
|||
storm::gspn::Place place = places.at(entry.first); |
|||
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INHIBITOR); |
|||
jsonGspn.push_back(jsonInputArc); |
|||
} |
|||
|
|||
// Export output arcs
|
|||
for (auto const& entry : transition.getOutputPlaces()) { |
|||
storm::gspn::Place place = places.at(entry.first); |
|||
modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::OUTPUT); |
|||
jsonGspn.push_back(jsonInputArc); |
|||
} |
|||
} |
|||
return jsonGspn; |
|||
} |
|||
|
|||
|
|||
modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) { |
|||
modernjson::json data; |
|||
data["id"] = toJsonString(place); |
|||
data["name"] = place.getName(); |
|||
data["marking"] = place.getNumberOfInitialTokens(); |
|||
|
|||
modernjson::json position; |
|||
position["x"] = x * scaleFactor; |
|||
position["y"] = y * scaleFactor; |
|||
|
|||
modernjson::json jsonPlace; |
|||
jsonPlace["data"] = data; |
|||
jsonPlace["position"] = position; |
|||
jsonPlace["group"] = "nodes"; |
|||
jsonPlace["classes"] = "place"; |
|||
return jsonPlace; |
|||
} |
|||
|
|||
modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y) { |
|||
modernjson::json data; |
|||
data["id"] = toJsonString(transition, true); |
|||
data["name"] = transition.getName(); |
|||
data["priority"] = transition.getPriority(); |
|||
data["weight"] = transition.getWeight(); |
|||
|
|||
modernjson::json position; |
|||
position["x"] = x * scaleFactor; |
|||
position["y"] = y * scaleFactor; |
|||
|
|||
modernjson::json jsonTrans; |
|||
jsonTrans["data"] = data; |
|||
jsonTrans["position"] = position; |
|||
jsonTrans["group"] = "nodes"; |
|||
jsonTrans["classes"] = "trans_im"; |
|||
return jsonTrans; |
|||
} |
|||
|
|||
modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y) { |
|||
modernjson::json data; |
|||
data["id"] = toJsonString(transition, false); |
|||
data["name"] = transition.getName(); |
|||
data["rate"] = transition.getRate(); |
|||
data["priority"] = transition.getPriority(); |
|||
|
|||
modernjson::json position; |
|||
position["x"] = x * scaleFactor; |
|||
position["y"] = y * scaleFactor; |
|||
|
|||
modernjson::json jsonTrans; |
|||
jsonTrans["data"] = data; |
|||
jsonTrans["position"] = position; |
|||
jsonTrans["group"] = "nodes"; |
|||
jsonTrans["classes"] = "trans_time"; |
|||
return jsonTrans; |
|||
} |
|||
|
|||
modernjson::json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) { |
|||
modernjson::json data; |
|||
data["id"] = toJsonString(transition, place, arctype); |
|||
data["source"] = toJsonString(place); |
|||
data["target"] = toJsonString(transition, immediate); |
|||
data["mult"] = multiplicity; |
|||
|
|||
modernjson::json jsonArc; |
|||
jsonArc["data"] = data; |
|||
//jsonTrans["group"] = "nodes";
|
|||
switch (arctype) { |
|||
case INPUT: |
|||
jsonArc["classes"] = "input"; |
|||
break; |
|||
case OUTPUT: |
|||
jsonArc["classes"] = "output"; |
|||
break; |
|||
case INHIBITOR: |
|||
jsonArc["classes"] = "inhibit"; |
|||
break; |
|||
default: |
|||
STORM_LOG_ASSERT(false, "Unknown type " << arctype << " used."); |
|||
} |
|||
return jsonArc; |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,71 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/utility/macros.h" |
|||
|
|||
#include "storm-gspn/storage/gspn/GSPN.h" |
|||
|
|||
// JSON parser |
|||
#include "json.hpp" |
|||
namespace modernjson { |
|||
using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>; |
|||
} |
|||
|
|||
namespace storm { |
|||
namespace gspn { |
|||
|
|||
/** |
|||
* Exports a GSPN into the JSON format for visualizing it. |
|||
*/ |
|||
class GspnJsonExporter { |
|||
|
|||
public: |
|||
static void toStream(storm::gspn::GSPN const& gspn, std::ostream& os); |
|||
|
|||
static modernjson::json translate(storm::gspn::GSPN const& gspn); |
|||
|
|||
private: |
|||
enum ArcType { INPUT, OUTPUT, INHIBITOR }; |
|||
|
|||
static modernjson::json translatePlace(storm::gspn::Place const& place, double x, double y); |
|||
|
|||
static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y); |
|||
|
|||
static modernjson::json translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y); |
|||
|
|||
static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype); |
|||
|
|||
std::string static inline toJsonString(storm::gspn::Place const& place) { |
|||
std::stringstream stream; |
|||
stream << "p" << place.getID(); |
|||
return stream.str(); |
|||
} |
|||
|
|||
std::string static inline toJsonString(storm::gspn::Transition const& transition, bool immediate) { |
|||
std::stringstream stream; |
|||
stream << (immediate ? "i" : "t") << transition.getID(); |
|||
return stream.str(); |
|||
} |
|||
|
|||
std::string static inline toJsonString(storm::gspn::Transition const& transition, storm::gspn::Place const& place, ArcType arctype) { |
|||
std::stringstream stream; |
|||
stream << place.getID(); |
|||
switch (arctype) { |
|||
case INPUT: |
|||
stream << "i"; |
|||
break; |
|||
case OUTPUT: |
|||
stream << "o"; |
|||
break; |
|||
case INHIBITOR: |
|||
stream << "h"; |
|||
break; |
|||
default: |
|||
STORM_LOG_ASSERT(false, "Unknown type " << arctype << " used."); |
|||
} |
|||
stream << transition.getID(); |
|||
return stream.str(); |
|||
} |
|||
}; |
|||
|
|||
} |
|||
} |
|||
@ -1,62 +0,0 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/storage/jani/Model.h" |
|||
|
|||
#include "storm-gspn/builder/JaniGSPNBuilder.h" |
|||
#include "storm-gspn/storage/gspn/GSPN.h" |
|||
|
|||
#include "storm/settings/SettingsManager.h" |
|||
#include "storm-gspn/settings/modules/GSPNExportSettings.h" |
|||
|
|||
#include "storm/utility/file.h" |
|||
|
|||
namespace storm { |
|||
/** |
|||
* Builds JANI model from GSPN. |
|||
*/ |
|||
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn) { |
|||
storm::builder::JaniGSPNBuilder builder(gspn); |
|||
return builder.build(); |
|||
} |
|||
|
|||
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) { |
|||
storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>(); |
|||
if (exportSettings.isWriteToDotSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToDotFilename(), fs); |
|||
gspn.writeDotToStream(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isWriteToPnproSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToPnproFilename(), fs); |
|||
gspn.toPnpro(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isWriteToPnmlSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteToPnmlFilename(), fs); |
|||
gspn.toPnml(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
if (exportSettings.isDisplayStatsSet()) { |
|||
std::cout << "============GSPN Statistics==============" << std::endl; |
|||
gspn.writeStatsToStream(std::cout); |
|||
std::cout << "=========================================" << std::endl; |
|||
} |
|||
|
|||
if (exportSettings.isWriteStatsToFileSet()) { |
|||
std::ofstream fs; |
|||
storm::utility::openFile(exportSettings.getWriteStatsFilename(), fs); |
|||
gspn.writeStatsToStream(fs); |
|||
storm::utility::closeFile(fs); |
|||
} |
|||
|
|||
|
|||
|
|||
} |
|||
|
|||
} |
|||
Some files were not shown because too many files changed in this diff
Reference in new issue
xxxxxxxxxx