Minimize.hh

Go to the documentation of this file.

#ifndef __DIADES__AUTOMATA__EXPERIMENTAL__MINIMIZE__HH
#define __DIADES__AUTOMATA__EXPERIMENTAL__MINIMIZE__HH

#include<unordered_map>
#include<set>
#include<diades/utils/Verbose.hh>
#include<diades/utils/Exceptions.hh>
#include<diades/automata/experimental/StateMachine.hh>
#include<diades/automata/experimental/Complete.hh>
#include<diades/automata/experimental/Determine.hh>
#include<diades/automata/experimental/StateCreation.hh>
#include<diades/automata/experimental/BeliefState.hh>
#include<diades/automata/experimental/Abstract.hh>

namespace Diades {
    namespace Automata {
        namespace Experimental {

            template<typename Fsm>
            bool
            splitPartition(const Fsm & machine,
                    const std::shared_ptr<BeliefState<Fsm>> bigQ0,
                    const std::shared_ptr<BeliefState<Fsm>> bigQ1,
                    typename Fsm::EventPropertyId littleA,
                    std::shared_ptr<BeliefState<Fsm>> bigQ0prime,
                    std::shared_ptr<BeliefState<Fsm>> bigQ0MinusbigQ0prime) {
                bool result = true;
                // first of all, if Q0 owns one state only, by definition it is not splittable
                // especially if Q0 owns the sink state { represented by an empty belief state }
                if (bigQ0->size() <= 1) {
                    result = false;
                } else {
                    // two cases, either bigQ1 is empty (this is the sink state) or not  (normal belief state)
                    for (auto state : bigQ0->setOfNodes()) {
                        auto transIt = machine.outputEventTransitionBegin(state, littleA);
                        if (transIt == machine.outputEventTransitionEnd(state, littleA)) {
                            // *transIt is actually the transition: 'state --littleA--> sinkState'
                            if (bigQ1->isEmpty()) {
                                bigQ0prime->insertNode(state);
                            } else {
                                bigQ0MinusbigQ0prime->insertNode(state);
                            }
                        } else {
                            // *transIt is a real transition from the machine: 'source --littleA--> target'
                            // and target is not the sink state
                            if (bigQ1->isEmpty()) {
                                bigQ0MinusbigQ0prime->insertNode(state);
                            } else {
                                // check whether transIt->target is in Q1 or not
                                if (bigQ1->findNode(transIt->target()) != bigQ1->end()) {
                                    bigQ0prime->insertNode(state);
                                } else {
                                    bigQ0MinusbigQ0prime->insertNode(state);
                                }
                            }
                        }

                        if ((bigQ0->size() == bigQ0prime->size()) ||
                                (bigQ0->size() == bigQ0MinusbigQ0prime->size())) {
                            // Not splittable
                            bigQ0prime->setOfNodes().clear();
                            bigQ0MinusbigQ0prime->setOfNodes().clear();
                            result = false;
                        }
                    }
                }
                return result;
            }

            template<typename Fsm>
            void
            nerodePartition(const Fsm & machine,
                    vector<std::shared_ptr<BeliefState<Fsm>>> & partition) {
                using BelState = BeliefState<Fsm>;
                using BelStatePtr = std::shared_ptr<BelState>;
                using EventInfo = typename Fsm::EventPropertyId;
                //using BsIterator = Diades::Utils::SharedPointerConstIterator<BelState, std::vector>;


                // Now we are ready to apply the Hopcroft algorithm on the partition
                // This algorithm is based on the description in
                // "A taxonomy of finite automata minimization algorithms" by Bruce W. Watson
                // watson@win.tue.nl
                if (isComplete(machine)) {
                    // the machine is complete. As there is no notion of acceptor
                    // states in this version of the algorithm, it means that
                    // all the states are acceptors. It results that
                    // the minimal DFA in this case in simply the universal 
                    // DFA (a partition of one elament with all the states in)
                    auto bs = std::make_shared<BelState>(machine);
                    bs->insertStates(machine.stateBegin(), machine.stateEnd());
                    partition.push_back(bs);
                } else {
                    // The current DFA is not complete, we must use a sink state to apply the algorithm
                    // We won't complete the DFA explicitely but implicitly by the use of an empty
                    // BeliefState pointer. In this version, all the states are acceptors EXCEPT
                    // the sink state. 
                    // Here partition represents variable P initialised with [ {non acceptor states}, {acceptor states} ]
                    auto sinkState = std::make_shared<BelState>(machine);
                    partition.push_back(sinkState); // I do not represent the sink state in the partition
                    auto allState = std::make_shared<BelState>(machine);
                    allState->insertStates(machine.stateBegin(), machine.stateEnd());
                    partition.push_back(allState);


                    // As the sink state is always part of a singleton in any
                    // computed partition, we start iterating with by putting in L
                    // L := sinkstate x letter1 , sinkstate x letter2, ....
                    std::unordered_map<EventInfo, std::set<BelStatePtr> > bigL;
                    // implements L: (Q,a) \in L iff bigL[a].find(Q) != bigL[a].end()
                    // initialise: L = F x V i.e {sinkState} x [eventBegin, eventEnd)
                    std::for_each(machine.eventBegin(), machine.eventEnd(),
                            [&](EventInfo e) {
                                bigL[e].insert(sinkState); });


                    while (!bigL.empty()) {
                        // Let (Q_1,a) : (Q_1,a) in L
                        EventInfo a = bigL.begin()->first;
                        BelStatePtr bigQ1 = *(bigL.begin()->second.begin());


                        // L:= L\{(Q_1,a)}
                        bigL.begin()->second.erase(bigL.begin()->second.begin());
                        if (bigL.begin()->second.empty()) {
                            bigL.erase(bigL.begin());
                        }

                        size_t oldPartitionSize = partition.size(); // I dont copy to P_old, no need

                        for (size_t index = 0; index < oldPartitionSize; ++index) // for Q_0 in P_old
                        {

                            auto bigQ0 = partition[index];
                            auto bigQ0prime = std::make_shared<BelState>(machine);
                            auto bigQ0MinusbigQ0prime = std::make_shared<BelState>(machine);
                            if (splitPartition(machine, bigQ0, bigQ1, a, bigQ0prime, bigQ0MinusbigQ0prime)) {
                                // it means that Splittable(Q_0,Q_1,a) and bigQ0prime is not empty
                                partition[index] = bigQ0prime;
                                partition.push_back(bigQ0MinusbigQ0prime); // P = P \ {Q0} \cup {Q0\Q0',Q0'}

                                for (auto littleB : machine.events()) {
                                    auto & bss = bigL[littleB];
                                    if (bss.find(bigQ0) != bss.end()) {

                                        bss.erase(bigQ0);
                                        bss.insert(bigQ0prime);
                                        bss.insert(bigQ0MinusbigQ0prime);
                                        // L = L \ {(Q0,b)} \cup {(Q0',b), (Q0 \ Q0',b)}
                                    } else {
                                        if (bigQ0prime->size() <= bigQ0MinusbigQ0prime->size()) {
                                            bss.insert(bigQ0prime);
                                        } else {
                                            bss.insert(bigQ0MinusbigQ0prime);
                                        }
                                        // L = L \cup {min( (Q0',b) , (Q0\Q0',b) ) }
                                    }
                                }
                            }
                        }

                    }
                }
            }

                        
            template<typename Fsm, typename StateCreator>
            void
            minimizeDeterministicMachine(const Fsm & machine,
                    Fsm & minimalMachine,
                    StateCreator & creator) {
                using Bs = BeliefState<Fsm>;
                using BsPointer = std::shared_ptr < Bs >;
                using BsIterator = Diades::Utils::SharedPointerIterator<Bs, std::vector>;
                std::vector<BsPointer> partition;
                // we compute the nerode partitition: i.e. the partition of states such that
                // for any Q0 Q1 there is no pair of state q0 and q'0 from Q0 such
                // that q0 - a -> q1 is a transition of 'machine' and q1 is in Q1
                // while q'0 - a -> q'1 is a transition of 'machine' and q'1 is NOT in Q1 
                nerodePartition(machine, partition);
                // once the partition is found, just abstract the machine
                // be aware that there might an empty belief state at the beginning of
                // partition (sink state)
                auto partIt = partition.begin();
                if ((*partIt)->isEmpty()) {
                    ++partIt;
                }
                abstract(machine, minimalMachine,
                        BsIterator(partIt),
                        BsIterator(partition.end()),
                        creator);
            }
                        
                        
                        
                        
                        
//            /**
//             * 
//             * @param machine The original StateMachine 
//             * @param minimalMachine The minimal version of the original StateMachine
//             * @pre minimalMachine must not be the original machine
//             * @pre Note that if the StateMachine does not have any initial state, it is considered
//             * as if the original StateMachine is empty. A StateMachine that has no
//             * 'specific' initial states is a StateMachine such any state can be initial, in this case
//             *  machine.setAllInitialStates() must be applied first.
//             * @pre machine must be deterministic (no check here)
//             * @post A minimal StateMachine, if not empty, has one initial state only.
//             */
//            template<typename Fsm>
//            void
//            minimizeDeterministicMachine(const Fsm & machine,
//                    Fsm & minimalMachine) {
//                using Bs = BeliefState<Fsm>;
//                using BsPointer = std::shared_ptr < Bs >;
//                using BsIterator = Diades::Utils::SharedPointerIterator<Bs, std::vector>;
//                std::vector<BsPointer> partition;
//                // we compute the nerode partitition: i.e. the partition of states such that
//                // for any Q0 Q1 there is no pair of state q0 and q'0 from Q0 such
//                // that q0 - a -> q1 is a transition of 'machine' and q1 is in Q1
//                // while q'0 - a -> q'1 is a transition of 'machine' and q'1 is NOT in Q1 
//                nerodePartition(machine, partition);
//                // once the partition is found, just abstract the machine
//                // be aware that there might an empty belief state at the beginning of
//                // partition (sink state)
//                auto partIt = partition.begin();
//                if ((*partIt)->isEmpty()) {
//                    ++partIt;
//                }
//                OnlyStateCreator<Fsm> creator(machine,minimalMachine);
//                abstract(machine, minimalMachine,
//                        BsIterator(partIt),
//                        BsIterator(partition.end()),creator);
//            }

//            /**
//             * 
//             * @param machine The original StateMachine 
//             * @param minimalMachine The minimal version of the original StateMachine
//             * @pre minimalMachine must not be the original machine
//             * @pre Note that if the StateMachine does not have any initial state, it is considered
//             * as if the original StateMachine is empty. A StateMachine that has no
//             * 'specific' initial states is a StateMachine such any state can be initial, in this case
//             *  machine.setAllInitialStates() must be applied first.
//             * @post A minimal StateMachine, if not empty, has one initial state only.
//             */
//            template<typename Fsm>
//            void
//            minimize(const Fsm & machine,
//                    Fsm & minimalMachine) {
//                if (machine.numberOfInitialStates() == 0) {
//                    minimalMachine.clear();
//                } else {
//                    if (!isDeterministic(machine)) {
//                        // the Hopcroft minimization algorithm only works on deterministic machines
//                        Fsm deterministicMachine;
//                        OnlyStateCreator<Fsm> creator(machine,deterministicMachine);
//                        determine(machine, deterministicMachine,creator);
//                        minimizeDeterministicMachine(deterministicMachine, minimalMachine);
//                    } else {
//                        minimizeDeterministicMachine(machine, minimalMachine);
//                    }
//                }
//            }


            template<typename Fsm, typename StateCreator>
            void
            minimize(const Fsm & machine,
                    Fsm & minimalMachine,
                    StateCreator & creator) {
                if (machine.numberOfInitialStates() == 0) {
                    minimalMachine.clear();
                } else {
                                        if(!isDeterministic(machine))
                                                {
                                                return;
                                                }
                                        else
                                        {
                        minimizeDeterministicMachine(machine,
                                minimalMachine,
                                creator);
                                                
                    }
                }
            }


        }
    }
}


#endif /* __DIADES__AUTOMATA__EXPERIMENTAL__MINIMIZE__HH */