diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp new file mode 100644 index 000000000..7ec2e1fb5 --- /dev/null +++ b/src/builder/JaniProgramGraphBuilder.cpp @@ -0,0 +1,7 @@ +#include "JaniProgramGraphBuilder.h" + +namespace storm { + namespace builder { + unsigned JaniProgramGraphBuilder::janiVersion = 1; + } +} \ No newline at end of file diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h new file mode 100644 index 000000000..01f392e47 --- /dev/null +++ b/src/builder/JaniProgramGraphBuilder.h @@ -0,0 +1,66 @@ +#include "src/storage/ppg/ProgramGraph.h" +#include "src/storage/jani/Model.h" +#include "src/storage/jani/Location.h" +#include "src/storage/IntegerInterval.h" + + +namespace storm { + namespace builder { + + enum class JaniProgramGraphVariableDomainMethod { + Unrestricted, IntervalPropagation + }; + + struct JaniProgramGraphBuilderSetting { + JaniProgramGraphVariableDomainMethod variableDomainMethod = JaniProgramGraphVariableDomainMethod::Unrestricted; + }; + + class JaniProgramGraphBuilder { + public: + static unsigned janiVersion; + + JaniProgramGraphBuilder() { + + } + + //void addVariableRestriction(storm::expressions::Variable const& var, storm::IntegerInterval const& interval ) { + + //} + + + + storm::jani::Model* build(storm::ppg::ProgramGraph const& pg, std::string const& name = "program_graph") { + expManager = pg.getExpressionManager(); + storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager); + storm::jani::Automaton mainAutomaton("main"); + addProcedureVariables(mainAutomaton, pg); + addProcedureLocations(mainAutomaton, pg); + model->addAutomaton(mainAutomaton); + return model; + } + + private: + void addProcedureVariables(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) { + for (auto const& v : pg.getVariables()) { + if(variableRestrictions.count(v.getIndex())) { + assert(false); + } else { + storm::jani::UnboundedIntegerVariable janiVar(v.getName(), v, expManager->integer(0), false); + automaton.addUnboundedIntegerVariable(janiVar); + } + } + } + + void addProcedureLocations(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) { + for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) { + storm::jani::Location janiLoc(std::to_string(it->second.id())); + automaton.addLocation(janiLoc); + } + } + + std::map variableRestrictions; + std::shared_ptr expManager; + + }; + } +} \ No newline at end of file diff --git a/src/storage/IntegerInterval.cpp b/src/storage/IntegerInterval.cpp new file mode 100644 index 000000000..7722d359b --- /dev/null +++ b/src/storage/IntegerInterval.cpp @@ -0,0 +1,2 @@ +#include "IntegerInterval.h" + diff --git a/src/storage/IntegerInterval.h b/src/storage/IntegerInterval.h new file mode 100644 index 000000000..6f59be238 --- /dev/null +++ b/src/storage/IntegerInterval.h @@ -0,0 +1,42 @@ +#pragma once + +#include + +namespace storm { + namespace storage { + class IntegerInterval { + + public: + explicit IntegerInterval(uint64_t v) : leftBound(v), rightBound(v) { + + } + + IntegerInterval(uint64_t lb, uint64_t rb) : leftBound(lb), rightBound(rb) { + + } + + bool hasLeftBound() { + return leftBound != boost::none; + } + + bool hasRightBound() { + return rightBound != boost::none; + } + + boost::optional getLeftBound() { + return leftBound; + } + + boost::optional getRightBound() { + return rightBound; + } + + private: + boost::optional leftBound; + boost::optional rightBound; + + }; + + std::ostream& operator<<(std::ostream& os, IntegerInterval const& i); + } +} \ No newline at end of file