diff options
author | Stefan Radomski <radomski@tk.informatik.tu-darmstadt.de> | 2014-10-20 07:20:16 (GMT) |
---|---|---|
committer | Stefan Radomski <radomski@tk.informatik.tu-darmstadt.de> | 2014-10-20 07:20:16 (GMT) |
commit | 59c9ae81b4911c6458cbe8a5ed78554bdcc82861 (patch) | |
tree | aab941294ccd67c8379f2dfb71ca107236d51f05 /src/uscxml/transform/ChartToFSM.h | |
parent | 9ba649b087df2bc161759e55549facc2f8f80878 (diff) | |
download | uscxml-59c9ae81b4911c6458cbe8a5ed78554bdcc82861.zip uscxml-59c9ae81b4911c6458cbe8a5ed78554bdcc82861.tar.gz uscxml-59c9ae81b4911c6458cbe8a5ed78554bdcc82861.tar.bz2 |
SCXML -> Promela skips intermediate explicit flat SCXML for ridiculous better memory footprint
Diffstat (limited to 'src/uscxml/transform/ChartToFSM.h')
-rw-r--r-- | src/uscxml/transform/ChartToFSM.h | 162 |
1 files changed, 84 insertions, 78 deletions
diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index 2f97a24..9e583b1 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -31,7 +31,33 @@ namespace uscxml { class GlobalState; class GlobalTransition; -class FlatteningInterpreter; +class ChartToFSM; + +class USCXML_API Complexity { +public: + Complexity() : value(0) {} + Complexity(uint64_t value) : value(value) {} + + Complexity& operator+=(const Complexity& rhs) { + value += rhs.value; + history.insert(history.end(), rhs.history.begin(), rhs.history.end()); + return *this; + } + + Complexity& operator*=(const Complexity& rhs) { + value *= rhs.value; + history.insert(history.end(), rhs.history.begin(), rhs.history.end()); + return *this; + } + + static uint64_t stateMachineComplexity(const Arabica::DOM::Element<std::string>& root); + +protected: + static Complexity calculateStateMachineComplexity(const Arabica::DOM::Element<std::string>& root); + + uint64_t value; + std::list<uint64_t> history; +}; class USCXML_API GlobalState { public: @@ -40,20 +66,25 @@ public: GlobalState(const Arabica::XPath::NodeSet<std::string>& activeStates, const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates, // we need to remember for binding=late const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates, - const std::string& xmlNSPrefix); - - Arabica::XPath::NodeSet<std::string> activeStates; - Arabica::XPath::NodeSet<std::string> alreadyEnteredStates; - std::map<std::string, Arabica::XPath::NodeSet<std::string> > historyStates; - - std::map<std::string, GlobalTransition*> incoming; - std::map<std::string, GlobalTransition*> outgoing; + const std::string& xmlNSPrefix, + ChartToFSM* flattener); + + std::set<int> activeStatesRefs; + std::set<int> alreadyEnteredStatesRefs; + std::map<std::string, std::set<int> > historyStatesRefs; + + Arabica::XPath::NodeSet<std::string> getActiveStates(); + Arabica::XPath::NodeSet<std::string> getAlreadyEnteredStates(); + std::map<std::string, Arabica::XPath::NodeSet<std::string> > getHistoryStates(); + + std::list<GlobalTransition*> sortedOutgoing; std::string stateId; + std::string activeId; - static int gIndex; - - std::string index; + long index; bool isFinal; + + ChartToFSM* interpreter; }; @@ -70,19 +101,17 @@ public: Arabica::DOM::Element<std::string> uninvoke; }; - GlobalTransition(const Arabica::XPath::NodeSet<std::string>& transitions, DataModel dataModel, FlatteningInterpreter* flattener); + GlobalTransition(const Arabica::XPath::NodeSet<std::string>& transitions, DataModel dataModel, ChartToFSM* flattener); bool isValid; // constructor will determine, calling code will delete if not bool isEventless; // whether or not all our transitions are eventless bool isTargetless; // whether or not all our transitions are eventless bool isSubset; // there is a superset to this set - -// std::vector<long> firstElemPerLevel; -// std::vector<long> nrElemPerLevel; -// std::vector<long> prioPerLevel; - - Arabica::XPath::NodeSet<std::string> transitions; // constituting transitions - + bool hasExecutableContent; + + std::set<int> transitionRefs; // indizes of constituting transitions + Arabica::XPath::NodeSet<std::string> getTransitions() const; + std::list<std::string> eventNames; // the list of longest event names that will enable this set std::string eventDesc; // space-seperated eventnames for convenience std::string condition; // conjunction of all the set's conditions @@ -91,18 +120,12 @@ public: // executable content we gathered when we took the transition std::list<Action> actions; - Arabica::XPath::NodeSet<std::string> entered; - Arabica::XPath::NodeSet<std::string> exited; - - Arabica::XPath::NodeSet<std::string> invoke; - Arabica::XPath::NodeSet<std::string> uninvoke; - std::string transitionId; std::string source; std::string destination; - std::string index; - FlatteningInterpreter* interpreter; + long index; + ChartToFSM* interpreter; bool operator< (const GlobalTransition& other) const; @@ -110,17 +133,23 @@ protected: std::list<std::string> getCommonEvents(const Arabica::XPath::NodeSet<std::string>& transitions); }; -class USCXML_API FlatteningInterpreter : public InterpreterRC, public InterpreterMonitor { + +class USCXML_API ChartToFSM : public InterpreterRC, public InterpreterMonitor { public: - FlatteningInterpreter(const Arabica::DOM::Document<std::string>& doc); - virtual ~FlatteningInterpreter(); + virtual ~ChartToFSM(); + +protected: + ChartToFSM(const Interpreter& other); Arabica::DOM::Document<std::string> getDocument() const; // overwrite to return flat FSM InterpreterState interpret(); + + Arabica::XPath::NodeSet<std::string> refsToStates(const std::set<int>&); + Arabica::XPath::NodeSet<std::string> refsToTransitions(const std::set<int>&); + + std::vector<Arabica::DOM::Element<std::string> > indexedTransitions; + std::vector<Arabica::DOM::Element<std::string> > indexedStates; - std::list<Arabica::DOM::Element<std::string> > indexedTransitions; - -protected: // gather executable content per microstep void executeContent(const Arabica::DOM::Element<std::string>& content, bool rethrow = false); @@ -140,61 +169,38 @@ protected: virtual void beforeTakingTransition(Interpreter interpreter, const Arabica::DOM::Element<std::string>& transition, bool moreComing); void explode(); + void getPotentialTransitionsForConf(const Arabica::XPath::NodeSet<std::string>& conf, std::map<std::string, GlobalTransition*>& outMap); void labelTransitions(); -// void weightTransitions(); - void createDocument(); void indexTransitions(const Arabica::DOM::Element<std::string>& root); std::list<GlobalTransition*> sortTransitions(std::list<GlobalTransition*> list); - void appendGlobalStateNode(GlobalState* globalState); - Arabica::DOM::Node<std::string> globalTransitionToNode(GlobalTransition* globalTransition); - - GlobalState* _start; - GlobalTransition* _currGlobalTransition; - - uint64_t _perfProcessed; - uint64_t _perfTotal; + // we need this static as we use it in a sort function + static std::map<Arabica::DOM::Node<std::string>, Arabica::DOM::Node<std::string> > _transParents; + + static bool filterSameState(const Arabica::XPath::NodeSet<std::string>& transitions); + + uint64_t _perfTransProcessed; + uint64_t _perfTransTotal; + uint64_t _perfStatesProcessed; + uint64_t _perfStatesSkippedProcessed; + uint64_t _perfStatesSkippedTotal; + uint64_t _perfStatesCachedProcessed; + uint64_t _perfStatesCachedTotal; uint64_t _lastTimeStamp; - int maxDepth; - int maxOrder; - size_t _lastTransientStateId; + size_t _lastStateIndex; + size_t _lastTransIndex; + GlobalState* _start; + GlobalTransition* _currGlobalTransition; Arabica::DOM::Document<std::string> _flatDoc; std::map<std::string, GlobalState*> _globalConf; -}; - -class USCXML_API ChartToFSM { -public: - static Interpreter flatten(const Interpreter& other); - static uint64_t stateMachineComplexity(const Arabica::DOM::Element<std::string>& root); - -protected: - class USCXML_API Complexity { - public: - Complexity() : value(0) {} - Complexity(uint64_t value) : value(value) {} - - Complexity& operator+=(const Complexity& rhs) { - value += rhs.value; - history.insert(history.end(), rhs.history.begin(), rhs.history.end()); - return *this; - } - - Complexity& operator*=(const Complexity& rhs) { - value *= rhs.value; - history.insert(history.end(), rhs.history.begin(), rhs.history.end()); - return *this; - } - - uint64_t value; - std::list<uint64_t> history; - }; - - static Complexity calculateStateMachineComplexity(const Arabica::DOM::Element<std::string>& root); - + std::map<std::string, GlobalState*> _transPerActiveConf; // potentially enabled transition sets per active configuration + + friend class GlobalTransition; + friend class GlobalState; }; } |