Unfolding.hh

Go to the documentation of this file.

#ifndef __DIADES__ALTARICA_UNFOLDING__HH
#define __DIADES__ALTARICA_UNFOLDING__HH

#include<graph/Graph.hh>
#include<graph/NodeMap.hh>
#include"Node.hh"
#include"Sdmdl.hh"
#include"NodeInstance.hh"

using namespace Diades::Graph;

namespace Diades
{
  namespace Altarica
  {

  
        typedef Diades::Graph::Node GNode;
  
        struct EncodedTransition
        {
          set<Event> triggers;
          Formula precondition;
          Formula postcondition;
        };
  
        struct Encoding
        {
          NodeInstance  node;
          list<Formula> invariant;
          list<EncodedTransition *> transitions;
          Formula initialisation;
          Formula initialStates;
          Diades::Graph::Graph   fsm;
          NodeMap<Formula> formula;
          vector< pair<Formula,GNode> > nodeFormula;
        };


 



  
        bool encodeInvariant(NodeInstance node,list<Formula> & invariantFormula);


        bool encodeNodeInstance(NodeInstance node);
                

        bool encodeTransitions(NodeInstance node,const list<Formula> & invariant,list<EncodedTransition *> & transitions);



        bool encodeInitialAssignments(NodeInstance node,Formula & initialisation);


        bool encodeInitialStates(NodeInstance node, const list<Formula> & invariant,Formula & initialisation, Formula & initialStates);


  };
};
#endif