system.h

Go to the documentation of this file.

// -*- mode: C++; c-file-style: "stroustrup"; c-basic-offset: 4; indent-tabs-mode: nil; -*-

/* libutap - Uppaal Timed Automata Parser.
   Copyright (C) 2011-2018 Aalborg University.
   Copyright (C) 2002-2006 Uppsala University and Aalborg University.

   This library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public License
   as published by the Free Software Foundation; either version 2.1 of
   the License, or (at your option) any later version.

   This library 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.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with this library; if not, write to the Free Software
   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
   USA
*/

#ifndef UTAP_INTERMEDIATE_HH
#define UTAP_INTERMEDIATE_HH

#include "utap/symbols.h"
#include "utap/expression.h"
#include "utap/position.h"

#include <list>
#include <deque>
#include <vector>
#include <map>
#include <exception>
#include <algorithm>

namespace UTAP
{
    struct variable_t
    {
        symbol_t uid;      
        expression_t expr; 
        std::string toString() const;
    };

    struct state_t
    {
        symbol_t uid;           
        expression_t invariant; 
        expression_t exponentialRate;
        expression_t costRate;  
        int32_t locNr;          
        std::string toString() const;
    };

    struct branchpoint_t
    {
        symbol_t uid;
        int32_t bpNr;
    };



    struct edge_t
    {
        int nr;                 
        bool control;           
        std::string actname;
        state_t *src;           
        branchpoint_t *srcb;    
        state_t *dst;           
        branchpoint_t *dstb;    
        frame_t select;         
        expression_t guard;     
        expression_t assign;    
        expression_t sync;      
#ifdef ENABLE_PROB
        expression_t prob;      
#endif
        std::string toString() const;
        std::list<int32_t> selectValues;  
    };

    class BlockStatement; // Forward declaration

    struct function_t
    {
        symbol_t uid;               
        std::set<symbol_t> changes; 
        std::set<symbol_t> depends; 
        std::list<variable_t> variables; 
        BlockStatement *body;       
        function_t() : body(NULL) {}
        ~function_t();
        std::string toString() const; // used to write the XML file
    };

    struct progress_t
    {
        expression_t guard;
        expression_t measure;
    };

    struct iodecl_t
    {
        std::string instanceName;
        std::vector<expression_t> param;
        std::list<expression_t> inputs, outputs, csp;
    };

    struct ganttmap_t
    {
        frame_t parameters;
        expression_t predicate, mapping;
    };

    struct gantt_t
    {
        gantt_t(const char *s) : name(s) {}
        gantt_t(const std::string& s) : name(s) {}

        std::string name;    
        frame_t parameters;  
        std::list<ganttmap_t> mapping;
    };

    struct template_t;
    struct declarations_t
    {
        frame_t frame;
        std::list<variable_t> variables;        
        std::list<function_t> functions;        
        std::list<progress_t> progress;         
        std::list<iodecl_t> iodecl;
        std::list<gantt_t> ganttChart;

        bool addFunction(type_t type, const std::string&, function_t *&);
        std::string toString(bool global = false) const;
        std::string getConstants() const;
        std::string getTypeDefinitions() const;
        std::string getVariables(bool global) const;
        std::string getFunctions() const;
    };

    struct instanceLine_t;  //to be defined later

    struct message_t
    {
        int nr = -1;                   
        int location;
        instanceLine_t *src;           
        instanceLine_t *dst;           
        expression_t label;            
        bool isInPrechart;
    };
    struct condition_t
    {
        int nr = -1;                        
        int location;
        std::vector<instanceLine_t*> anchors;       //TODO
        expression_t label;            
        bool isInPrechart;
        bool isHot;
    };

    struct update_t
    {
        int nr = -1;                   
        int location;
        instanceLine_t *anchor;        
        expression_t label;            
        bool isInPrechart;
    };

    struct simregion_t
    {
        int nr;
        message_t* message;              
        condition_t* condition;          
        update_t* update;                
        int getLoc() const;
        bool isInPrechart() const;

        simregion_t()
        {
            message = new message_t();
            condition = new condition_t();
            update = new update_t();
        }

        ~simregion_t()
        {
            delete message;
            delete condition;
            delete update;
        }

        std::string toString() const;

        void setMessage(std::deque<message_t>& messages, int nr);
        void setCondition(std::deque<condition_t>& conditions, int nr);
        void setUpdate(std::deque<update_t>& updates, int nr);
    };

    struct compare_simregion
    {
        bool operator() (const simregion_t& x, const simregion_t& y) const
        {
            return (x.getLoc() < y.getLoc());
        }
    };

    struct cut_t
    {
        int nr;
        std::vector<simregion_t> simregions; //unordered
        cut_t(int number) {
            simregions.clear();
            nr = number;
        };
        void add(simregion_t s) {
            simregions.push_back(s);
        };
        void erase(simregion_t s);
        bool contains(simregion_t s);

        bool isInPrechart(const simregion_t& fSimregion) const;
        bool isInPrechart() const;

        bool equals(const cut_t& y) const;

        std::string toString() const {
            std::string s="CUT(";
            for (unsigned int i = 0; i < simregions.size(); ++i)
                s += simregions[i].toString() + " ";
            s = s.substr(0, s.size()-1);
            s += ")";
            return s;
        };
    };

    struct instance_t
    {
        symbol_t uid;                             
        frame_t parameters;                       
        std::map<symbol_t, expression_t> mapping; 
        size_t arguments;
        size_t unbound;
        struct template_t *templ;
        std::set<symbol_t> restricted;            
        std::string writeMapping() const ;
        std::string writeParameters() const ;
        std::string writeArguments() const ;
    };

    struct instanceLine_t : public instance_t
    {
        int32_t instanceNr;         
        std::vector<simregion_t> getSimregions(const std::vector<simregion_t>& simregions);
        void addParameters(instance_t &inst, frame_t params,
            const std::vector<expression_t> &arguments);
    };

    struct template_t : public instance_t, declarations_t
    {
        symbol_t init;                           
        frame_t templateset;                     
        std::deque<state_t> states;              
        std::deque<branchpoint_t> branchpoints;  
        std::deque<edge_t> edges;                
        std::vector<expression_t> dynamicEvals;
        bool isTA;

        int addDynamicEval (expression_t t) {
            dynamicEvals.push_back (t);
            return dynamicEvals.size()-1;
        }

        std::vector<expression_t>& getDynamicEval () {return dynamicEvals;}

        state_t &addLocation(const std::string&, expression_t inv, expression_t er);

        branchpoint_t &addBranchpoint(const std::string&);

        edge_t &addEdge(symbol_t src, symbol_t dst, bool type,
                        const std::string& actname);

        std::deque<instanceLine_t> instances;    
        std::deque<message_t> messages;          
        std::deque<update_t> updates;            
        std::deque<condition_t> conditions;      
        std::string type;
        std::string mode;
        bool hasPrechart;
        bool dynamic;
        int dynindex;
        bool isDefined;

        instanceLine_t &addInstanceLine();

        message_t &addMessage(symbol_t src, symbol_t dst, int loc, bool pch);

        condition_t &addCondition(std::vector<symbol_t> anchors, int loc,
                bool pch, bool isHot);

        update_t &addUpdate(symbol_t anchor, int loc, bool pch);

        bool isInvariant(); // type of the LSC


        /* gets the simregions from the LSC scenario */
        const std::vector<simregion_t> getSimregions();

        /* returns the condition on the given instance, at y location */
        bool getCondition(instanceLine_t* instance, int y, condition_t*& simCondition);

        /* returns the update on the given instance at y location */
        bool getUpdate(instanceLine_t* instance, int y, update_t*& simUpdate);

        /* returns the first update on one of the given instances, at y location */
        bool getUpdate(const std::vector<instanceLine_t*>& instances, int y, update_t*& simUpdate);
       
    };

    struct chan_priority_t
    {
        typedef std::pair<char,expression_t> entry;
        typedef std::list<entry> tail_t;

        expression_t head; 
        tail_t       tail; 

        std::string toString() const;
    };

    struct query_t {
        std::string formula;
        std::string comment;
        std::string location;
    };
    typedef std::vector<query_t> queries_t;


    class TimedAutomataSystem;

    class SystemVisitor
    {
    public:
        virtual ~SystemVisitor() {}
        virtual void visitSystemBefore(TimedAutomataSystem *) {}
        virtual void visitSystemAfter(TimedAutomataSystem *) {}
        virtual void visitVariable(variable_t &) {}
        virtual bool visitTemplateBefore(template_t &) { return true; }
        virtual void visitTemplateAfter(template_t &) {}
        virtual void visitState(state_t &) {}
        virtual void visitEdge(edge_t &) {}
        virtual void visitInstance(instance_t &) {}
        virtual void visitProcess(instance_t &) {}
        virtual void visitFunction(function_t &) {}
        virtual void visitTypeDef(symbol_t) {}
        virtual void visitIODecl(iodecl_t&) {}
        virtual void visitProgressMeasure(progress_t &) {}
        virtual void visitGanttChart(gantt_t&) {}
        virtual void visitInstanceLine(instanceLine_t &) {}
        virtual void visitMessage(message_t &) {}
        virtual void visitCondition(condition_t &) {}
        virtual void visitUpdate(update_t &) {}
    };

    class TimedAutomataSystem
    {
    public:
        TimedAutomataSystem();
        TimedAutomataSystem(const TimedAutomataSystem&);
        virtual ~TimedAutomataSystem();

        declarations_t &getGlobals();

        std::list<template_t> &getTemplates();
        std::vector<template_t*> &getDynamicTemplates ();
        template_t* getDynamicTemplate(const std::string& name);

        std::list<instance_t> &getProcesses();

        queries_t &getQueries();

        void addPosition(
            uint32_t position, uint32_t offset, uint32_t line, const std::string& path);
        const Positions::line_t &findPosition(uint32_t position) const;

        variable_t *addVariableToFunction(
            function_t *, frame_t, type_t, const std::string&, expression_t initital);
        variable_t *addVariable(
            declarations_t *, type_t type, const std::string&, expression_t initial);
        void addProgressMeasure(
            declarations_t *, expression_t guard, expression_t measure);

        template_t &addTemplate(const std::string&, frame_t params,
                                const bool isTA = true,
                                const std::string& type = "",
                                const std::string& mode = "");
        template_t &addDynamicTemplate(const std::string&, frame_t params);

        instance_t &addInstance(
            const std::string& name, instance_t &instance, frame_t params,
            const std::vector<expression_t> &arguments);

        instance_t &addLscInstance(
                const std::string& name, instance_t &instance, frame_t params,
                const std::vector<expression_t> &arguments);
        void removeProcess(instance_t &instance); //LSC

        void copyVariablesFromTo(template_t* from, template_t* to) const;
        void copyFunctionsFromTo(template_t* from, template_t* to) const;

        std::string obsTA; //name of the observer TA instance

        void addProcess(instance_t &instance);
        void addGantt(declarations_t*, gantt_t&);
        void accept(SystemVisitor &);

        void setBeforeUpdate(expression_t);
        expression_t getBeforeUpdate();
        void setAfterUpdate(expression_t);
        expression_t getAfterUpdate();

        void addQuery(const query_t &query);
        bool queriesEmpty();

        /* The default priority for channels is also used for 'tau
         * transitions' (i.e. non-synchronizing transitions).
         */
        void beginChanPriority(expression_t chan);
        void addChanPriority(char separator, expression_t chan);
        const std::list<chan_priority_t>& getChanPriorities() const;
        std::list<chan_priority_t>& getMutableChanPriorities();

        void setProcPriority(const char* name, int priority);

        int getProcPriority(const char* name) const;

        bool hasPriorityDeclaration() const;

        bool hasStrictInvariants() const;

        void recordStrictInvariant();

        bool hasStopWatch() const;

        void recordStopWatch();

        bool hasStrictLowerBoundOnControllableEdges() const;

        void recordStrictLowerBoundOnControllableEdges();

        void clockGuardRecvBroadcast() { hasGuardOnRecvBroadcast = true; }
        bool hasClockGuardRecvBroadcast() const { return hasGuardOnRecvBroadcast; }
        void setSyncUsed(sync_use_t s) { syncUsed = s; }
        sync_use_t getSyncUsed() const { return syncUsed; }

        void setUrgentTransition() { hasUrgentTrans = true; }
        bool hasUrgentTransition() const { return hasUrgentTrans; }
        bool hasDynamicTemplates () const {return dynamicTemplates.size () != 0;}

    protected:

        bool hasUrgentTrans;
        bool hasPriorities;
        bool hasStrictInv;
        bool stopsClock;
        bool hasStrictLowControlledGuards;
        bool hasGuardOnRecvBroadcast;
        int defaultChanPriority;
        std::list<chan_priority_t> chanPriorities;
        std::map<std::string,int> procPriority;
        sync_use_t syncUsed; // see typechecker

        // The list of templates.
        std::list<template_t> templates;
        //List of dynamic template
        std::list<template_t> dynamicTemplates;
        std::vector<template_t*> dynamicTemplatesVec;

        // The list of template instances.
        std::list<instance_t> instances;

        std::list<instance_t> lscInstances;
        bool modified;

        // List of processes.
        std::list<instance_t> processes;

        // Global declarations
        declarations_t global;

        expression_t beforeUpdate;
        expression_t afterUpdate;
        queries_t queries;

        variable_t *addVariable(
            std::list<variable_t> &variables, frame_t frame,
            type_t type, const std::string&);

        std::string location;

    public:
        void addError(position_t, const std::string& msg, const std::string& ctx="");
        void addWarning(position_t, const std::string& msg, const std::string& ctx="");
        bool hasErrors() const;
        bool hasWarnings() const;
        const std::vector<error_t> &getErrors() const;
        const std::vector<error_t> &getWarnings() const;
        void clearErrors();
        void clearWarnings();
        bool isModified() const;
        void setModified(bool mod);
        iodecl_t* addIODecl();
    private:
        std::vector<error_t> errors;
        std::vector<error_t> warnings;
        Positions positions;
    };
}

#endif