diff options
Diffstat (limited to 'src/uscxml/transform/ChartToPromela.h')
-rw-r--r-- | src/uscxml/transform/ChartToPromela.h | 447 |
1 files changed, 0 insertions, 447 deletions
diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h deleted file mode 100644 index 82c4e5d..0000000 --- a/src/uscxml/transform/ChartToPromela.h +++ /dev/null @@ -1,447 +0,0 @@ -/** - * @file - * @author 2012-2014 Stefan Radomski (stefan.radomski@cs.tu-darmstadt.de) - * @copyright Simplified BSD - * - * @cond - * This program is free software: you can redistribute it and/or modify - * it under the terms of the FreeBSD license as published by the FreeBSD - * project. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. - * - * You should have received a copy of the FreeBSD license along with this - * program. If not, see <http://www.opensource.org/licenses/bsd-license>. - * @endcond - */ - -#ifndef CHARTTOPROMELA_H_RP48RFDJ -#define CHARTTOPROMELA_H_RP48RFDJ - -#include "Transformer.h" -#include "ChartToFSM.h" -#include "uscxml/interpreter/InterpreterDraft6.h" -#include "uscxml/dom/DOMUtils.h" -#include "uscxml/util/Trie.h" - -#include <DOM/Document.hpp> -#include <DOM/Node.hpp> -#include <XPath/XPath.hpp> -#include <ostream> - -namespace uscxml { - -class PromelaCodeAnalyzer; -class ChartToPromela; -class PromelaParserNode; - -class USCXML_API PromelaInline { -public: - enum PromelaInlineType { - PROMELA_NIL = 0x0000, - PROMELA_LTL = 0x0001, - PROMELA_CODE = 0x0002, - PROMELA_EVENT_ALL_BUT = 0x0004, - PROMELA_EVENT_ONLY = 0x0008, - PROMELA_PROGRESS_LABEL = 0x0010, - PROMELA_ACCEPT_LABEL = 0x0020, - PROMELA_END_LABEL = 0x0040 - }; - - PromelaInline(const Arabica::DOM::Node<std::string>& node); - virtual ~PromelaInline() {} - - operator bool() { - return (type != PROMELA_NIL); - } - - std::list<PromelaInline*> children; - PromelaInline* prevSibling; - PromelaInline* nextSibling; - - virtual void dump(); - - virtual bool relatesTo(const Arabica::DOM::Node<std::string>& node) { - return container == node; - } - - size_t level; - std::string content; - Arabica::DOM::Element<std::string> container; - PromelaInlineType type; - -protected: - PromelaInline() : prevSibling(NULL), nextSibling(NULL), type(PROMELA_NIL) {}; -}; - -class USCXML_API PromelaInlines { -public: - - PromelaInlines(const Arabica::DOM::Node<std::string>& node); - PromelaInlines() {} - - virtual ~PromelaInlines(); - - std::list<PromelaInline*> getRelatedTo(const Arabica::DOM::Node<std::string>& node, PromelaInline::PromelaInlineType type); - std::list<PromelaInline*> getAllOfType(uint32_t type); - - std::map<Arabica::DOM::Node<std::string>, std::list<PromelaInline*> > inlines; - std::list<PromelaInline*> allInlines; - - static std::list<std::string> getStringLiterals(const Data& data); - static std::list<std::string> getEventNames(const Data& data); - - -}; - -class USCXML_API PromelaEventSource : public PromelaInline { -public: - PromelaEventSource(const PromelaInline& pmlInline) { - type = pmlInline.type; - container = pmlInline.container; - content = pmlInline.content; - events = Data::fromJSON(pmlInline.content); - } - - virtual bool relatesTo(const Arabica::DOM::Node<std::string>& node) { - return container == node || InterpreterImpl::isDescendant(node, container); - } - - Data events; -}; - -#if 0 - - -class USCXML_API PromelaInlinesAutoEvents : public PromelaInline { -public: - virtual ~PromelaInlinesAutoEvents() {} - virtual bool relatesTo(const Arabica::DOM::Node<std::string>&); - virtual void setContent(const std::string& content); - virtual void dump(); - - std::map<std::string, Data> states; -}; - - -class USCXML_API PromelaEventSource { -public: - - enum PromelaEventSourceType { - PROMELA_EVENT_SOURCE_INVALID, - PROMELA_EVENT_SOURCE_INVOKER, - PROMELA_EVENT_SOURCE_GLOBAL, - }; - - PromelaEventSource(); - PromelaEventSource(const PromelaInline& source, PromelaCodeAnalyzer* analyzer = NULL, uint32_t externalQueueLength = 0); - - void writeStart(std::ostream& stream, int indent = 0); - void writeStop(std::ostream& stream, int indent = 0); - void writeDeclarations(std::ostream& stream, int indent = 0); - void writeBody(std::ostream& stream); - - operator bool() { - return type != PROMELA_EVENT_SOURCE_INVALID; - } - - PromelaInline source; - std::string name; - uint32_t externalQueueLength; - uint32_t longestSequence; - - Arabica::DOM::Node<std::string> container; - std::list<std::list<std::string> > sequences; - PromelaEventSourceType type; - PromelaCodeAnalyzer* analyzer; -}; - -#endif - -class USCXML_API PromelaCodeAnalyzer { -public: - class PromelaTypedef { - public: - PromelaTypedef() : arraySize(0), minValue(0), maxValue(0) {} - std::string name; - std::string type; - size_t arraySize; - size_t minValue; - size_t maxValue; - std::map<std::string, PromelaTypedef> types; - std::set<ChartToPromela*> occurrences; - - bool operator==(const PromelaTypedef& other) const { - return name == other.name; - } - - }; - - PromelaCodeAnalyzer() : _eventTrie("."), _lastStrIndex(1), _lastStateIndex(0), _lastEventIndex(1), _usesInPredicate(false), _usesPlatformVars(false) { - } - - void addCode(const std::string& code, ChartToPromela* interpreter); - void addEvent(const std::string& eventName); - void addState(const std::string& stateName); - void addOrigState(const std::string& stateName); - void addLiteral(const std::string& stateName, int forceIndex = -1); - - bool usesComplexEventStruct() { - return _typeDefs.types.find("_event") != _typeDefs.types.end() && _typeDefs.types["_event"].types.size() > 0; - } - bool usesEventField(const std::string& fieldName) { - if (usesComplexEventStruct() && _typeDefs.types["_event"].types.find(fieldName) != _typeDefs.types["_event"].types.end()) - return true; - return false; - } - - bool usesEventDataField(const std::string& fieldName) { - if (usesComplexEventStruct() && - _typeDefs.types["_event"].types.find("data") != _typeDefs.types["_event"].types.end() && - _typeDefs.types["_event"].types["data"].types.find(fieldName) != _typeDefs.types["_event"].types["data"].types.end()) - return true; - return false; - } - - std::string getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, const std::string padding = ""); - std::string getTypeReset(const std::string& var, const PromelaTypedef& type, const std::string padding = ""); - - bool usesInPredicate() { - return _usesInPredicate; - } - void usesInPredicate(bool value) { - _usesInPredicate = value; - } - bool usesPlatformVars() { - return _usesPlatformVars; - } - - std::string macroForLiteral(const std::string& literal); - int indexForLiteral(const std::string& literal); - - std::set<std::string> getLiterals() { - return _strLiterals; - } - std::set<std::string> getEventsWithPrefix(const std::string& prefix); - std::map<std::string, int>& getEvents() { - return _events; - } - - std::map<std::string, int>& getStates() { - return _states; - } - - std::map<std::string, int>& getOrigStates() { - return _origStateIndex; - } - - - Trie& getTrie() { - return _eventTrie; - } - - std::string adaptCode(const std::string& code, const std::string& prefix); - - static std::string prefixIdentifiers(const std::string& expr, const std::string& prefix); - static std::list<std::pair<size_t, size_t> > getTokenPositions(const std::string& expr, int type, PromelaParserNode* ast); - - PromelaTypedef& getTypes() { - return _typeDefs; - } - - PromelaTypedef& getType(const std::string& typeName) { - return _typeDefs.types.at(typeName); - } - -protected: - std::string createMacroName(const std::string& literal); - int enumerateLiteral(const std::string& literal, int forceIndex = -1); - - std::set<std::string> _strLiterals; // all string literals - std::map<std::string, std::string> _strMacroNames; // macronames for string literals - std::map<std::string, int> _strIndex; // integer enumeration for string - std::map<std::string, int> _origStateIndex; // state enumeration for original states - - std::map<std::string, int> _states; - std::map<std::string, int> _events; - - PromelaTypedef _typeDefs; - Trie _eventTrie; - -private: - std::set<std::string> _macroNameSet; // helper set for uniqueness of macros - int _lastStrIndex; - int _lastStateIndex; - int _lastEventIndex; - bool _usesInPredicate; - bool _usesPlatformVars; -}; - -class ExecContentSeqItem { -public: - enum ExecContentType { - EXEC_CONTENT_ALL_BUT, - EXEC_CONTENT_ONLY_FOR, - EXEC_CONTENT_EVERY - }; - - ExecContentSeqItem(ExecContentType type, const std::set<GlobalTransition*>& transitions, const GlobalTransition::Action& action) - : type(type), transitions(transitions), action(action) {} - ExecContentSeqItem(ExecContentType type, GlobalTransition* transition, const GlobalTransition::Action& action) - : type(type), action(action) { - transitions.insert(transition); - } - - ExecContentType type; - std::set<GlobalTransition*> transitions; - GlobalTransition::Action action; -}; - -class HistoryTransitionClass { -public: - HistoryTransitionClass(GlobalTransition* transition); - HistoryTransitionClass(const std::string& from, const std::string& to); - - void init(const std::string& from, const std::string& to); - - std::map<std::string, std::set<std::string> > toRemember; - std::map<std::string, std::set<std::string> > toKeep; - std::map<std::string, std::set<std::string> > toForget; - - std::set<GlobalTransition*> members; - - - void merge(const HistoryTransitionClass& other); - bool matches(const HistoryTransitionClass& other); -}; - -class USCXML_API ChartToPromela : public TransformerImpl, public ChartToFSM { -public: - - virtual ~ChartToPromela(); - static Transformer transform(const Interpreter& other); - - void writeTo(std::ostream& stream); - -protected: - ChartToPromela(const Interpreter& other) - : TransformerImpl(), - ChartToFSM(other), - _analyzer(NULL), - _allowEventInterleaving(false), - _hasIndexLessLoops(false), - _writeTransitionPrintfs(false), - _traceTransitions(false), - _machinesAll(NULL), - _parent(NULL), - _parentTopMost(NULL), - _machinesAllPerId(NULL), - _perfTransProcessed(0), - _perfTransTotal(0), - _perfHistoryProcessed(0), - _perfHistoryTotal(0), - _perfStatesProcessed(0), - _perfStatesTotal(0), - _lastTimeStamp(0) {} - - void initNodes(); - - static std::string beautifyIndentation(const std::string& code, int indent = 0); - - void writeProgram(std::ostream& stream); - - void writeEvents(std::ostream& stream); - void writeStates(std::ostream& stream); - void writeStateMap(std::ostream& stream); - void writeHistoryArrays(std::ostream& stream); - void writeTypeDefs(std::ostream& stream); - void writeStrings(std::ostream& stream); - void writeDeclarations(std::ostream& stream); - void writeEventSources(std::ostream& stream); - void writeTransition(std::ostream& stream, GlobalTransition* transition, int indent = 0); - std::string conditionalizeForHist(const std::set<GlobalTransition*>& transitions, int indent = 0); - std::string conditionalizeForHist(GlobalTransition* transition, int indent = 0); - void writeHistoryAssignments(std::ostream& stream, GlobalTransition* transition, int indent = 0); - void writeTransitionClosure(std::ostream& stream, GlobalTransition* transition, GlobalState* state, int indent = 0); - - void writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent = 0); - void writeInlineComment(std::ostream& stream, const Arabica::DOM::Node<std::string>& node); - void writeFSM(std::ostream& stream); - void writeEventDispatching(std::ostream& stream); - void writeMain(std::ostream& stream); - - void writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent = 0); - void writeDispatchingBlock(std::ostream& stream, std::list<GlobalTransition*>, int indent = 0); - - void writeStartInvoker(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, ChartToPromela* invoker, int indent = 0); - //void writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent = 0, bool atomic = true); - - void writeDetermineShortestDelay(std::ostream& stream, int indent = 0); - void writeInsertWithDelay(std::ostream& stream, int indent = 0); - void writeAdvanceTime(std::ostream& stream, int indent = 0); - void writeRescheduleProcess(std::ostream& stream, int indent = 0); - void writeScheduleMachines(std::ostream& stream, int indent = 0); - void writeCancelEvents(std::ostream& stream, int indent = 0); - void writeRemovePendingEventsFromInvoker(std::ostream& stream, int indent = 0); - - std::list<GlobalTransition::Action> getTransientContent(GlobalTransition* transition); - //Arabica::DOM::Node<std::string> getUltimateTarget(const Arabica::DOM::Element<std::string>& transition); - - static std::string declForRange(const std::string& identifier, long minValue, long maxValue, bool nativeOnly = false); - static std::string conditionForHistoryTransition(const GlobalTransition* transition); - -// std::string replaceStringsInExpression(const std::string& expr); - - std::string sanitizeCode(const std::string& code); - std::string dataToAssignments(const std::string& prefix, const Data& data); - -// Arabica::XPath::NodeSet<std::string> _globalStates; -// Arabica::DOM::Node<std::string> _startState; -// std::map<std::string, Arabica::DOM::Element<std::string> > _states; -// std::map<Arabica::DOM::Element<std::string>, int> _transitions; - - std::list<std::string> _varInitializers; // pending initializations for arrays - - PromelaCodeAnalyzer* _analyzer; - bool _allowEventInterleaving; - bool _hasIndexLessLoops; - bool _writeTransitionPrintfs; - bool _traceTransitions; - - uint32_t _externalQueueLength; - uint32_t _internalQueueLength; - - PromelaInlines pmlInlines; -// std::map<std::string, PromelaEventSource> _invokers; -// PromelaEventSource _globalEventSource; - - std::map<std::string, std::map<std::string, size_t> > _historyMembers; // ids of all history states - std::set<std::string> _dataModelVars; - - Arabica::DOM::Node<std::string> _finalize; - std::map<Arabica::DOM::Node<std::string>, ChartToPromela*> _machines; - std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>* _machinesAll; - ChartToPromela* _parent; // our invoking interpreter - ChartToPromela* _parentTopMost; - - std::map<std::string, Arabica::DOM::Node<std::string> > _machinesPerId; - std::map<std::string, Arabica::DOM::Node<std::string> >* _machinesAllPerId; - std::string _prefix; // our prefix in case of nested SCXML documents - std::string _invokerid; - - uint64_t _perfTransProcessed; - uint64_t _perfTransTotal; - uint64_t _perfHistoryProcessed; - uint64_t _perfHistoryTotal; - uint64_t _perfStatesProcessed; - uint64_t _perfStatesTotal; - uint64_t _lastTimeStamp; - - friend class PromelaEventSource; -}; - -} - -#endif /* end of include guard: CHARTTOPROMELA_H_RP48RFDJ */ |