diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index f22760db8..e5f1e9b0b 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -8,6 +8,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Edge.h" #include "storm/settings/SettingsManager.h" diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 1b162d3bb..816500023 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -7,6 +7,8 @@ #include "storm/storage/BitVector.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Edge.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 2c308559c..18dd15d6e 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -6,7 +6,12 @@ #include "storm/logic/Formulas.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" diff --git a/src/storm/builder/DdJaniModelBuilder.h b/src/storm/builder/DdJaniModelBuilder.h index aca9f5650..371b52557 100644 --- a/src/storm/builder/DdJaniModelBuilder.h +++ b/src/storm/builder/DdJaniModelBuilder.h @@ -6,7 +6,6 @@ #include "storm/logic/Formula.h" -#include "storm/storage/jani/Model.h" namespace storm { namespace models { @@ -15,6 +14,9 @@ namespace storm { class Model; } } + namespace jani { + class Model; + } namespace builder { diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index ae0067042..b207816bb 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -18,6 +18,16 @@ #include "storm/generator/PrismNextStateGenerator.h" #include "storm/generator/JaniNextStateGenerator.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" +#include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/ParallelComposition.h" +#include "storm/storage/jani/CompositionInformationVisitor.h" + #include "storm/utility/prism.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 15805419b..3c029aee0 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -5,9 +5,16 @@ #include #include "storm/solver/SmtSolver.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" -#include "storm/storage/jani/JSONExporter.h" +#include "storm/storage/jani/CompositionInformationVisitor.h" + #include "storm/builder/RewardModelInformation.h" diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index 062865459..65321ad9f 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -28,6 +28,14 @@ namespace storm { class StandardRewardModel; } } + + namespace jani { + class OrderedAssignments; + class Assignment; + class Variable; + class Edge; + class EdgeDestination; + } namespace builder { namespace jit { diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index efdb54d42..d9b83074e 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -5,6 +5,8 @@ #include "storm/storage/SymbolicModelDescription.h" + + #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index d53974178..63f81526a 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -6,6 +6,16 @@ #include "storm/solver/SmtSolver.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" +#include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/ParallelComposition.h" +#include "storm/storage/jani/CompositionInformationVisitor.h" + #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 4e8652166..2d15e887b 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -3,8 +3,14 @@ #include "storm/generator/NextStateGenerator.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/OrderedAssignments.h" namespace storm { + namespace jani { + class Edge; + class EdgeDestination; + } + namespace generator { template diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index d904ae545..2cfd5911c 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -2,6 +2,8 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/jani/Model.h" + +#include "storm/storage/jani/Automaton.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index b1468d87a..0d53828eb 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -10,6 +10,16 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/VariableSetPredicateSplitter.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" +#include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/ParallelComposition.h" +#include "storm/storage/jani/CompositionInformationVisitor.h" + #include "storm/storage/dd/DdManager.h" #include "storm/abstraction/prism/PrismMenuGameAbstractor.h" diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 8fac23926..99f1993d4 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -1,8 +1,15 @@ #include "JaniParser.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/TemplateEdge.h" +#include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" #include "storm/storage/jani/Property.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" +#include "storm/storage/jani/CompositionInformationVisitor.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/InvalidJaniException.h" diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 92b52c783..e602e9300 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -4,6 +4,10 @@ #include "storm/utility/prism.h" #include "storm/utility/jani.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" + + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidTypeException.h" diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 7817fea56..23d27cc6a 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -1,5 +1,9 @@ #include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/TemplateEdge.h" +#include "storm/storage/jani/Location.h" + #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index d9bd2a517..6c940d464 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -7,14 +7,15 @@ #include #include "storm/storage/jani/VariableSet.h" -#include "storm/storage/jani/Edge.h" -#include "storm/storage/jani/TemplateEdge.h" -#include "storm/storage/jani/Location.h" + namespace storm { namespace jani { class Automaton; + class Edge; + class TemplateEdge; + class Location; namespace detail { class Edges { diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 982d4a51f..fbc7426b3 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -2,8 +2,17 @@ #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/storage/jani/Compositions.h" + +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/TemplateEdge.h" +#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Location.h" +#include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" +#include "storm/storage/jani/Compositions.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" @@ -22,7 +31,11 @@ namespace storm { const std::string Model::SILENT_ACTION_NAME = ""; const uint64_t Model::SILENT_ACTION_INDEX = 0; - + + + Model::Model(Model&& other) = default; + Model& Model::operator=(Model&& other) = default; + Model::Model() { // Intentionally left empty. } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index e942743bd..201e1ecc5 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -2,11 +2,18 @@ #include + +#include + +#include "storm/storage/jani/VariableSet.h" #include "storm/storage/jani/Action.h" #include "storm/storage/jani/ModelType.h" #include "storm/storage/jani/Automaton.h" #include "storm/storage/jani/Constant.h" #include "storm/storage/jani/Composition.h" +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/Location.h" +#include "storm/storage/jani/TemplateEdge.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" @@ -17,7 +24,13 @@ namespace storm { } namespace jani { - + + class Variable; + class BooleanVariable; + class BoundedIntegerVariable; + class UnboundedIntegerVariable; + class RealVariable; + class Automaton; class Exporter; class SynchronizationVector; @@ -45,8 +58,8 @@ namespace storm { */ Model& operator=(Model const& other); - Model(Model&& other) = default; - Model& operator=(Model&& other) = default; + Model(Model&& other); + Model& operator=(Model&& other); /*! * Retrieves the expression manager responsible for the expressions in the model. diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 23e3215f7..6bc39b83c 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -5,6 +5,7 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/prism/CompositionToJaniVisitor.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/TemplateEdge.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h"