@@ -691,8 +691,8 @@ class FiniteStateMachine : public Abstract::FiniteStateMachine {
691691 using EquivalenceMap = std::map<const Abstract::State*,
692692 std::shared_ptr<Abstract::SetOfStateRefs>>;
693693
694- // minimize the automaton based on edge labels only .
695- std::shared_ptr<FiniteStateMachine<StateLabelType, EdgeLabelType>> minimizeEdgeLabels () {
694+ // minimize the automaton based on edge and state labels .
695+ std::shared_ptr<FiniteStateMachine<StateLabelType, EdgeLabelType>> minimizeEdgeLabels (bool ignoreStateLabels = false ) {
696696 // partition refinement algorithm
697697
698698 // generate a vector of equivalence classes
@@ -709,8 +709,58 @@ class FiniteStateMachine : public Abstract::FiniteStateMachine {
709709 eqMap[sp] = initialClass;
710710 }
711711
712- // partition refinement
712+ // partition on state labels
713+
713714 bool changed = false ;
715+ if (! ignoreStateLabels) {
716+ do {
717+ changed = false ;
718+
719+ std::list<std::shared_ptr<Abstract::SetOfStateRefs>> newEqClasses;
720+
721+ // for every potential equivalence class
722+ for (const auto &ic : eqClasses) {
723+ std::shared_ptr<Abstract::SetOfStateRefs> _class = ic;
724+
725+ auto i = _class->begin ();
726+
727+ // pick arbitrary state from class
728+ auto s1 = dynamic_cast <const State<StateLabelType, EdgeLabelType> *>(*i);
729+
730+ std::shared_ptr<Abstract::SetOfStateRefs> equivSet =
731+ std::make_shared<Abstract::SetOfStateRefs>();
732+ std::shared_ptr<Abstract::SetOfStateRefs> remainingSet =
733+ std::make_shared<Abstract::SetOfStateRefs>();
734+ equivSet->insert (s1);
735+
736+ // check whether all other states have the same label.
737+ while (++i != _class->end ()) {
738+ auto s2 = dynamic_cast <const State<StateLabelType, EdgeLabelType> *>(*i);
739+ if (s1->getLabel () == s2->getLabel ()) {
740+ equivSet->insert (s2);
741+ } else {
742+ remainingSet->insert (s2);
743+ }
744+ }
745+ // if not, split the class
746+ if (equivSet->size () == _class->size ()) {
747+ newEqClasses.push_back (equivSet);
748+ this ->mapStates (eqMap, equivSet);
749+ } else {
750+ newEqClasses.push_back (equivSet);
751+ this ->mapStates (eqMap, equivSet);
752+ newEqClasses.push_back (remainingSet);
753+ this ->mapStates (eqMap, remainingSet);
754+ changed = true ;
755+ }
756+ }
757+ auto tempEqClasses = eqClasses;
758+ eqClasses = newEqClasses;
759+ } while (changed);
760+ }
761+
762+ // partition refinement on transitions
763+ changed = false ;
714764 do {
715765 changed = false ;
716766
@@ -818,8 +868,8 @@ class FiniteStateMachine : public Abstract::FiniteStateMachine {
818868 std::shared_ptr<Abstract::SetOfStateRefs> ns1 = s1->nextStatesOfEdgeLabel (l);
819869 std::shared_ptr<Abstract::SetOfStateRefs> ns2 = s2->nextStatesOfEdgeLabel (l);
820870 // collect classes of states in ns1 and ns2
821- std::set<SetOfStates<StateLabelType, EdgeLabelType> * > cs1;
822- std::set<SetOfStates<StateLabelType, EdgeLabelType> * > cs2;
871+ std::set<std::shared_ptr<Abstract::SetOfStateRefs> > cs1;
872+ std::set<std::shared_ptr<Abstract::SetOfStateRefs> > cs2;
823873 for (auto j : *ns1) {
824874 auto s = j;
825875 cs1.insert (m[s]);
@@ -846,38 +896,12 @@ class FiniteStateMachine : public Abstract::FiniteStateMachine {
846896};
847897} // namespace Labeled
848898
849- // Edge Labelled Scenario Automaton
850- using ELSState = ::FSM::Labeled::State<CId, CString>;
851- using ELSEdge = ::FSM::Labeled::Edge<CId, CString>;
852- using ELSSetOfStates = ::FSM::Labeled::SetOfStates<CId, CString>;
853- using ELSSetOfEdges = ::FSM::Abstract::SetOfEdges;
854- using ELSSetOfStateRefs = ::FSM::Abstract::SetOfStateRefs;
855- using ELSSetOfEdgeRefs = ::FSM::Abstract::SetOfEdgeRefs;
856-
857- class EdgeLabeledScenarioFSM : public ::FSM::Labeled::FiniteStateMachine<CId, CString> {
858- public:
859- EdgeLabeledScenarioFSM () = default ;
860- ~EdgeLabeledScenarioFSM () override = default ;
861-
862- EdgeLabeledScenarioFSM (const EdgeLabeledScenarioFSM &) = delete ;
863- EdgeLabeledScenarioFSM &operator =(const EdgeLabeledScenarioFSM &other) = delete ;
864- EdgeLabeledScenarioFSM (EdgeLabeledScenarioFSM &&) = delete ;
865- EdgeLabeledScenarioFSM &operator =(EdgeLabeledScenarioFSM &&) = delete ;
866-
867- virtual void removeDanglingStates ();
868- };
869899
870900namespace StateStringLabeled {
871901
872902// make an FSM class with unlabeled edges, based on the labeled one with some dummy char labels
873903//
874904
875- // class SetOfEdges : public Labeled::SetOfEdges<CString, char> {};
876- // class SetOfEdgeRefs : public Labeled::SetOfEdgeRefs<CString, char> {};
877-
878- // class SetOfStates : public Labeled::SetOfStates<CString, char> {};
879- // class SetOfStateRefs : public Labeled::SetOfStateRefs<CString, char> {};
880-
881905class State : public Labeled ::State<CString, char > {
882906public:
883907 explicit State (const CString &withLabel) : Labeled::State<CString, char>(withLabel) {}
0 commit comments