JaniGSPNBuilder.h

Go to the documentation of this file.

#pragma once
 
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/Property.h"
 
namespace storm {
namespace builder {
class JaniGSPNBuilder {
   public:
    JaniGSPNBuilder(storm::gspn::GSPN const& gspn) : gspn(gspn), expressionManager(gspn.getExpressionManager()) {}
 
    virtual ~JaniGSPNBuilder() {
        // Intentionally left empty.
    }
 
    storm::jani::Model* build(std::string const& automatonName = "gspn_automaton");
 
    storm::jani::Variable const& getPlaceVariable(uint64_t placeId) const {
        return *vars.at(placeId);
    }
 
    std::vector<storm::jani::Property> getStandardProperties(storm::jani::Model* model, std::shared_ptr<storm::logic::AtomicExpressionFormula> atomicFormula,
                                                             std::string name, std::string description, bool maximal);
 
    std::vector<storm::jani::Property> getDeadlockProperties(storm::jani::Model* model);
 
    storm::jani::Variable const& addTransientVariable(storm::jani::Model* model, std::string name, storm::expressions::Expression expression);
 
   private:
    void addVariables(storm::jani::Model* model);
 
    uint64_t addLocation(storm::jani::Automaton& automaton);
 
    void addEdges(storm::jani::Automaton& automaton, uint64_t locId);
 
    storm::jani::Variable const& addDeadlockTransientVariable(storm::jani::Model* model, std::string name, bool ignoreCapacities = false,
                                                              bool ignoreInhibitorArcs = false, bool ignoreEmptyPlaces = false);
 
    const uint64_t janiVersion = 1;
    storm::gspn::GSPN const& gspn;
    std::map<uint64_t, storm::jani::Variable const*> vars;
    std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
};
}  // namespace builder
}  // namespace storm