BddStateMachineEncoding.hh

Go to the documentation of this file.

#ifndef __DIADES__SDMDL_EXPERIMENTAL__BDDSTATEMACHINEENCODING__HH__
#define __DIADES__SDMDL_EXPERIMENTAL__BDDSTATEMACHINEENCODING__HH__

#include <vector>
#include<diades/utils/Exceptions.hh>
#include<diades/sdmdl/Formula.hh>
#include<diades/automata/experimental/Event.hh>
#include<diades/automata/experimental/StateMachine.hh>
#include<diades/sdmdl/experimental/BddStateMachine.hh>

namespace Diades
{
    namespace Sdmdl
    {
        namespace Experimental
        {

            template<typename StateProperty, typename FaultProperty>
            BddStateMachine &
            encodeTransitions(const Diades::Automata::Experimental::StateMachine<StateProperty, FaultProperty> & component,
                              BddStateMachine & result)
            {
                for (auto it = component.transitionBegin();
                        it != component.transitionEnd();
                        ++it)
                {
                    stringstream stream1;
                    stream1 << component.getEvent(*it);
                    const Formula & event = result.event(result.eventVariable().getValue(stream1.str()));
                    stringstream stream2;
                    stream2 << component.getStatePropertyId(it->source());
                    const Formula & source = result.factory().newFormula(result.stateVariable(),
                                                                         result.stateVariable().getValue(stream2.str()));



                    stringstream stream3;
                    stream3 << component.getStatePropertyId(it->target());
                    const Formula & target = result.factory().newFormula(result.nextStateVariable(),
                                                                         result.nextStateVariable().getValue(stream3.str()));
                    result.addTransitions(source && target && event);
                }
                return result;
            }

            template<typename StateProperty, typename FaultProperty>
            BddStateMachine &
            encodeEvent(const Diades::Automata::Experimental::StateMachine<StateProperty, FaultProperty> & component,
                        BddStateMachine & result)
            {
                for (auto & evt: component.events())
                {
                    result.addEvent(evt);
                }
                return result;
            }

            template<typename StateProperty, typename FaultProperty>
            BddStateMachine &
            encodeInitialStates(const Diades::Automata::Experimental::StateMachine<StateProperty, FaultProperty> & component,

                                BddStateMachine & result)
            {

                for (auto it = component.initialStateBegin();
                        it != component.initialStateEnd(); ++it)
                {
                    stringstream stream;
                    stream << component.getStatePropertyId(*it);
                    result.addInitialStates(result.factory().newFormula(result.stateVariable(), 
                                                                        result.stateVariable().getValue(stream.str())));
                }
                                return result;
            }

            template<typename StateProperty, typename FaultProperty>
            BddStateMachine &
            encode(const Diades::Automata::Experimental::StateMachine<StateProperty, FaultProperty> & component,
                   Variable & stateVar,
                   Variable & nextStateVar,
                   Variable & event,
                   BddStateMachine & result)
            {
                result.clear();
                result.setEventVariable(event);
                result.setStateVariable(stateVar);
                result.setNextStateVariable(nextStateVar);
                result.resetInternalFormulaFactory();
                encodeEvent(component, result);
                encodeInitialStates(component, result);
                encodeTransitions(component,result);
                                return result;
            }
        };
    }
}



#endif