From 7485b7175b1e894e15172fa0188848512c4bac84 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Thu, 30 May 2024 15:41:46 +0200 Subject: [PATCH] fix gmp --- .../counterexamples/Counterexample.cpp | 31 ++++++++++--------- .../counterexamples/CounterexampleMdp.cpp | 4 ++- payntbind/src/synthesis/decpomdp/DecPomdp.h | 8 +++-- payntbind/src/synthesis/pomdp/PomdpManager.h | 5 +-- .../synthesis/pomdp/PomdpManagerAposteriori.h | 6 ++-- .../synthesis/pomdp_family/ProductPomdpFsc.h | 1 + .../pomdp_family/ProductPomdpRandomizedFsc.h | 1 + .../synthesis/translation/SubPomdpBuilder.h | 2 ++ 8 files changed, 34 insertions(+), 24 deletions(-) diff --git a/payntbind/src/synthesis/counterexamples/Counterexample.cpp b/payntbind/src/synthesis/counterexamples/Counterexample.cpp index b7ec7304c..2bcc08990 100644 --- a/payntbind/src/synthesis/counterexamples/Counterexample.cpp +++ b/payntbind/src/synthesis/counterexamples/Counterexample.cpp @@ -1,25 +1,26 @@ #include "Counterexample.h" -#include "storm/storage/BitVector.h" -#include "storm/exceptions/UnexpectedException.h" +#include +#include +#include -#include "storm/storage/sparse/JaniChoiceOrigins.h" -#include "storm/storage/sparse/StateValuations.h" +#include +#include -#include "storm/utility/builder.h" -#include "storm/storage/SparseMatrix.h" -#include "storm/storage/sparse/ModelComponents.h" -#include "storm/models/sparse/StateLabeling.h" +#include +#include +#include +#include -#include "storm/solver/OptimizationDirection.h" +#include -#include "storm/api/verification.h" -#include "storm/logic/Bound.h" -#include "storm/modelchecker/CheckTask.h" -#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include +#include +#include +#include -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" +#include +#include #include diff --git a/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp b/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp index 746187d20..e7152b057 100644 --- a/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp +++ b/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp @@ -1,7 +1,9 @@ #include "CounterexampleMdp.h" #include -#include +#include +#include + #include #include #include diff --git a/payntbind/src/synthesis/decpomdp/DecPomdp.h b/payntbind/src/synthesis/decpomdp/DecPomdp.h index 3341f3b99..6a76ba9fe 100644 --- a/payntbind/src/synthesis/decpomdp/DecPomdp.h +++ b/payntbind/src/synthesis/decpomdp/DecPomdp.h @@ -3,9 +3,10 @@ #include "madp/src/base/POMDPDiscrete.h" #include "madp/src/base/DecPOMDPDiscrete.h" -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/Pomdp.h" -#include "storm/models/sparse/StandardRewardModel.h" +#include +#include +#include +#include #include @@ -19,6 +20,7 @@ namespace synthesis { class DecPomdp { public: + DecPomdp(DecPOMDPDiscrete *model); /** Number of agents. */ diff --git a/payntbind/src/synthesis/pomdp/PomdpManager.h b/payntbind/src/synthesis/pomdp/PomdpManager.h index 9ed59ad17..46f30c98b 100644 --- a/payntbind/src/synthesis/pomdp/PomdpManager.h +++ b/payntbind/src/synthesis/pomdp/PomdpManager.h @@ -1,7 +1,8 @@ #pragma once -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/Pomdp.h" +#include +#include +#include namespace synthesis { diff --git a/payntbind/src/synthesis/pomdp/PomdpManagerAposteriori.h b/payntbind/src/synthesis/pomdp/PomdpManagerAposteriori.h index 2c624201f..9f361bba7 100644 --- a/payntbind/src/synthesis/pomdp/PomdpManagerAposteriori.h +++ b/payntbind/src/synthesis/pomdp/PomdpManagerAposteriori.h @@ -1,11 +1,11 @@ #pragma once -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/Pomdp.h" +#include +#include +#include #include - namespace synthesis { template diff --git a/payntbind/src/synthesis/pomdp_family/ProductPomdpFsc.h b/payntbind/src/synthesis/pomdp_family/ProductPomdpFsc.h index ea7836d2c..701371af7 100644 --- a/payntbind/src/synthesis/pomdp_family/ProductPomdpFsc.h +++ b/payntbind/src/synthesis/pomdp_family/ProductPomdpFsc.h @@ -2,6 +2,7 @@ #include "src/synthesis/translation/ItemKeyTranslator.h" +#include #include #include #include diff --git a/payntbind/src/synthesis/pomdp_family/ProductPomdpRandomizedFsc.h b/payntbind/src/synthesis/pomdp_family/ProductPomdpRandomizedFsc.h index 72612eb47..f1227c3b6 100644 --- a/payntbind/src/synthesis/pomdp_family/ProductPomdpRandomizedFsc.h +++ b/payntbind/src/synthesis/pomdp_family/ProductPomdpRandomizedFsc.h @@ -2,6 +2,7 @@ #include "src/synthesis/translation/ItemKeyTranslator.h" +#include #include #include #include diff --git a/payntbind/src/synthesis/translation/SubPomdpBuilder.h b/payntbind/src/synthesis/translation/SubPomdpBuilder.h index 5317750ad..b8e572cef 100644 --- a/payntbind/src/synthesis/translation/SubPomdpBuilder.h +++ b/payntbind/src/synthesis/translation/SubPomdpBuilder.h @@ -2,6 +2,8 @@ #include "src/synthesis/translation/ItemTranslator.h" +#include +#include #include namespace synthesis {