TAPAAL · srba · Sep 17, 2024 · Apr 16, 2024 · Apr 16, 2024 · Apr 16, 2024
diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml
@@ -35,5 +35,5 @@ jobs:
           cmakeGenerator: UnixMakefiles
           buildDirectory: '${{runner.workspace}}/build'
         env:
-          CC: gcc-11
-          CXX: g++-11
+          CC: gcc-12
+          CXX: g++-12
diff --git a/include/Colored/ColoredNetStructures.h b/include/Colored/ColoredNetStructures.h
@@ -25,6 +25,28 @@
 namespace unfoldtacpn {
     namespace Colored {
 
+        namespace SMC {
+            enum Distribution {
+                Constant,
+                Uniform,
+                Exponential,
+                Normal,
+                Gamma,
+                Erlang,
+                DiscreteUniform,
+                Geometric
+            };
+            struct DistributionParameters {
+                double param1;
+                double param2;
+            };
+            enum FiringMode {
+                Oldest, 
+                Youngest,
+                Random
+            };
+        }
+
         struct Arc {
             uint32_t place;
             uint32_t transition;
@@ -50,6 +72,10 @@ namespace unfoldtacpn {
             GuardExpression_ptr guard;
             int player;
             bool urgent;
+            SMC::Distribution distribution;
+            SMC::DistributionParameters distributionParams;
+            double weight;
+            SMC::FiringMode firingMode;
             std::vector<Arc> arcs;
             std::vector<TransportArc> transport;
         };

diff --git a/include/Colored/ColoredPetriNetBuilder.h b/include/Colored/ColoredPetriNetBuilder.h
@@ -39,7 +39,11 @@ namespace unfoldtacpn {
                            int player,
                            bool urgent,
                            double x,
-                           double y);
+                           double y,
+                           Colored::SMC::Distribution distrib = Colored::SMC::Constant,
+                           Colored::SMC::DistributionParameters params = { 0.0, 0.0 },
+                           double weight = 1.0,
+                           Colored::SMC::FiringMode firingMode = Colored::SMC::Oldest);
         void addArc(const std::string& source, const std::string& target,
                     int weight, bool inhibitor, const unfoldtacpn::Colored::ArcExpression_ptr &expr,
                                              const std::vector<unfoldtacpn::Colored::TimeInterval>& intervals);

diff --git a/include/PQL/SMCExpressions.h b/include/PQL/SMCExpressions.h
@@ -0,0 +1,47 @@
+#ifndef SMCEXPRESSIONS_H
+#define SMCEXPRESSIONS_H
+
+#include "Expressions.h"
+
+namespace unfoldtacpn::PQL {
+
+    struct SMCSettings {
+        int timeBound;
+        int stepBound;
+        float falsePositives;
+        float falseNegatives;
+        float indifferenceRegionUp;
+        float indifferenceRegionDown;
+        float confidence;
+        float estimationIntervalWidth;
+        bool compareToFloat;
+        float geqThan;
+    };
+
+    class ProbaCondition : public SimpleQuantifierCondition {
+    public:
+        ProbaCondition(SMCSettings settings, Condition_ptr cond)
+        : SimpleQuantifierCondition(cond) {
+            _settings = settings;
+        }
+        void analyze(NamingContext& context) override;
+        virtual const SMCSettings settings() const { return _settings; }
+    protected:
+        SMCSettings _settings;
+    };
+
+    class PFCondition : public ProbaCondition {
+    public:
+        using ProbaCondition::ProbaCondition;
+        void visit(Visitor&) const override;
+    };
+
+    class PGCondition : public ProbaCondition {
+    public:
+        using ProbaCondition::ProbaCondition;
+        void visit(Visitor&) const override;
+    };
+
+}
+
+#endif
diff --git a/include/PQL/Visitor.h b/include/PQL/Visitor.h
@@ -13,6 +13,7 @@
 #define VISITOR_H
 
 #include "PQL/Expressions.h"
+#include "PQL/SMCExpressions.h"
 
 #include <type_traits>
 #include <cassert>
@@ -55,6 +56,8 @@ namespace unfoldtacpn
             virtual void _accept(const AXCondition*);
             virtual void _accept(const EUCondition*);
             virtual void _accept(const AUCondition*);
+            virtual void _accept(const PFCondition*);
+            virtual void _accept(const PGCondition*);
 
             // shallow elements, neither of these should exist in a compiled expression
             virtual void _accept(const KSafeCondition* element);

diff --git a/include/PQL/XMLPrinter.h b/include/PQL/XMLPrinter.h
@@ -73,6 +73,10 @@ namespace unfoldtacpn {
 
             void _accept(const AFCondition *condition) override;
 
+            void _accept(const PGCondition *condition) override;
+
+            void _accept(const PFCondition *condition) override;
+
             void _accept(const EXCondition *condition) override;
 
             void _accept(const AXCondition *condition) override;

diff --git a/include/PetriParse/PNMLParser.h b/include/PetriParse/PNMLParser.h
@@ -80,6 +80,7 @@ class PNMLParser {
     void parseValue(rapidxml::xml_node<>* element, std::string& text);
     uint32_t parseNumberConstant(rapidxml::xml_node<>* element);
     void parsePosition(rapidxml::xml_node<>* element, double& x, double& y);
+    std::tuple<Colored::SMC::Distribution, Colored::SMC::DistributionParameters> parseDistribution(rapidxml::xml_node<>* element);
     bool isTransition(const std::string& s);
     void checkKeyword(const char* id);
     unfoldtacpn::ColoredPetriNetBuilder* _builder;

diff --git a/include/PetriParse/QueryXMLParser.h b/include/PetriParse/QueryXMLParser.h
@@ -30,6 +30,8 @@
 
 #include "PNMLParser.h"
 #include "QueryParser.h"
+#include "PQL/SMCExpressions.h"
+
 using namespace unfoldtacpn::PQL;
 
 class QueryXMLParser {
@@ -47,6 +49,8 @@ class QueryXMLParser {
     bool parseTags(rapidxml::xml_node<>*  element);
     Condition_ptr parseFormula(rapidxml::xml_node<>*  element);
     Condition_ptr parseBooleanFormula(rapidxml::xml_node<>*  element);
+    SMCSettings parseSmcSettings(rapidxml::xml_node<>* smcNode);
+    Condition_ptr parseSmcFormula(SMCSettings settings, rapidxml::xml_node<>* element);
     Expr_ptr parseIntegerExpression(rapidxml::xml_node<>*  element);
     std::string parsePlace(rapidxml::xml_node<>*  element);
     void fatal_error(const std::string& token);

diff --git a/include/TAPNBuilderInterface.h b/include/TAPNBuilderInterface.h
@@ -39,7 +39,8 @@ namespace unfoldtacpn {
 
         // add a time transition with a unique name
         virtual void addTransition(const std::string &name, int player, bool urgent,
-                                            double, double) = 0;
+                                            double, double, 
+                                            int distrib = 0, double distribParam1 = 1, double distribParam2 = 1, double weight = 1.0, int firingMode = 0) = 0;
 
         /* Add timed colored input arc with given arc expression*/
         virtual void addInputArc(const std::string &place,

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -15,7 +15,7 @@ install(TARGETS unfoldtacpn PQL Colored PetriParse
     ARCHIVE DESTINATION lib/unfoldtacpn)
 
 install(FILES ../include/unfoldtacpn.h ../include/TAPNBuilderInterface.h DESTINATION include/)
-install(FILES ../include/PQL/PQL.h ../include/PQL/Visitor.h ../include/PQL/Expressions.h  DESTINATION include/PQL/)
+install(FILES ../include/PQL/PQL.h ../include/PQL/Visitor.h ../include/PQL/Expressions.h ../include/PQL/SMCExpressions.h  DESTINATION include/PQL/)
 install(FILES ../include/Colored/ColoredNetStructures.h
               ../include/Colored/ColoredPetriNetBuilder.h
               ../include/Colored/Colors.h

diff --git a/src/Colored/ColoredPetriNetBuilder.cpp b/src/Colored/ColoredPetriNetBuilder.cpp
@@ -61,10 +61,14 @@ namespace unfoldtacpn {
             int player,
             bool urgent,
             double x,
-            double y) {
+            double y,
+            Colored::SMC::Distribution distrib,
+            Colored::SMC::DistributionParameters params,
+            double weight,
+            Colored::SMC::FiringMode firingMode) {
         if (_transitionnames.count(name) == 0) {
             uint32_t next = _transitionnames.size();
-            _transitions.emplace_back(Colored::Transition {name, guard, player, urgent});
+            _transitions.emplace_back(Colored::Transition {name, guard, player, urgent, distrib, params, weight, firingMode});
             _transitionnames[name] = next;
             _transitionlocations.push_back(std::tuple<double, double>(x,y));
         }
@@ -314,7 +318,8 @@ namespace unfoldtacpn {
                 (*_output_stream) << "   </transition>\n";
             }
 
-            builder.addTransition(name, transition.player, transition.urgent, std::get<0>(transitionPos), std::get<1>(transitionPos) + offset);
+            builder.addTransition(name, transition.player, transition.urgent, std::get<0>(transitionPos), std::get<1>(transitionPos) + offset, 
+                transition.distribution, transition.distributionParams.param1, transition.distributionParams.param2, transition.weight, transition.firingMode);
             _pttransitionnames[transition.name].push_back(name);
             for (auto& arc : transition.arcs) {
                 unfoldArc(builder, arc, b, name);

diff --git a/src/PQL/CMakeLists.txt b/src/PQL/CMakeLists.txt
@@ -8,5 +8,5 @@ bison_target(pql_parser "${CMAKE_CURRENT_SOURCE_DIR}/PQLQueryParser.y"
 
 add_flex_bison_dependency(pql_lexer pql_parser)
 
-add_library(PQL OBJECT ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp XMLPrinter.cpp Visitor.cpp)
+add_library(PQL OBJECT ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp XMLPrinter.cpp Visitor.cpp SMCExpressions.cpp)
 
diff --git a/src/PQL/Expressions.cpp b/src/PQL/Expressions.cpp
@@ -98,6 +98,12 @@ namespace unfoldtacpn {
             _cond2->analyze(context);
         }
 
+        /*void ProbaCompCondition::analyze(NamingContext &context) 
+        {
+            _cond1->analyze(context);
+            _cond2->analyze(context);
+        }*/
+
         void LogicalCondition::analyze(NamingContext& context) {
             for(auto& c : _conds) c->analyze(context);
         }
@@ -239,7 +245,7 @@ namespace unfoldtacpn {
         void UnfoldedIdentifierExpr::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
-        }
+        }        
 
         void MinusExpr::visit(Visitor& ctx) const
         {

diff --git a/src/PQL/PQLQueryParser.y b/src/PQL/PQLQueryParser.y
@@ -24,13 +24,13 @@ void pqlqerror(const char *s) { printf("ERROR: %s\n", s); std::exit(-1); }
 }
 
 /* Terminal type definition */
-%token <string> ID INT
-%token <token> DEADLOCK TRUE FALSE
-%token <token> LPAREN RPAREN
+%token <string> ID INT FLOAT
+%token <token> DEADLOCK TRUE FALSE COUNT
+%token <token> LPAREN RPAREN LBRACK RBRACK
 %token <token> AND OR NOT
 %token <token> EQUAL NEQUAL LESS LESSEQUAL GREATER GREATEREQUAL
 %token <token> PLUS MINUS MULTIPLY
-%token <token> EF AG AF EG CONTROL COLON
+%token <token> EF AG AF EG PF PG CONTROL COLON
 
 /* Terminal associativity */
 %left AND OR
@@ -89,4 +89,4 @@ term	: term MULTIPLY factor	{ $$ = new MultiplyExpr(std::vector<Expr_ptr>({Expr_
 factor	: LPAREN expr RPAREN	{ $$ = $2; }
 		| INT			{ $$ = new LiteralExpr(atol($1->c_str())); delete $1; }
 		| ID			{ $$ = new IdentifierExpr(*$1); delete $1; }
-		;
+		;
diff --git a/src/PQL/PQLQueryTokens.l b/src/PQL/PQLQueryTokens.l
@@ -26,24 +26,27 @@ digit         [0-9]
 letter        [a-zA-Z_]
 %%
 
-[ \t\n\r]         ;
-"true"            {return TOKEN(TRUE);}
-"false"           {return TOKEN(FALSE);}
-"deadlock"          {return TOKEN(DEADLOCK);}
-"and"           {return TOKEN(AND);}
-"AND"           {return TOKEN(AND);}
-"or"            {return TOKEN(OR);}
-"OR"            {return TOKEN(OR);}
-"not"           {return TOKEN(NOT);}
-"NOT"           {return TOKEN(NOT);}
+[ \t\n\r]         			;
+"true"            			{return TOKEN(TRUE);}
+"false"           			{return TOKEN(FALSE);}
+"deadlock"          		{return TOKEN(DEADLOCK);}
+"and"           			{return TOKEN(AND);}
+"AND"           			{return TOKEN(AND);}
+"or"            			{return TOKEN(OR);}
+"OR"            			{return TOKEN(OR);}
+"not"           			{return TOKEN(NOT);}
+"NOT"           			{return TOKEN(NOT);}
 "AG"						{return TOKEN(AG);}
 "EG"						{return TOKEN(EG);}
 "AF"						{return TOKEN(AF);}
 "EF"						{return TOKEN(EF);}
+"PG"						{return TOKEN(PG);}
+"PF"						{return TOKEN(PF);}
 "control"                   {return TOKEN(CONTROL);}
 {letter}({letter}|{digit})* {SAVE_TOKEN; return ID;}
-{digit}+          {SAVE_TOKEN; return INT;}
-(\"(\\.|[^"])*\") {SAVE_QUOTED_TOKEN; return ID;}
+{digit}+          			{SAVE_TOKEN; return INT;}
+{digit}+\.{digit}+			{SAVE_TOKEN; return FLOAT;}
+(\"(\\.|[^"])*\") 			{SAVE_QUOTED_TOKEN; return ID;}
 "&&"						{return TOKEN(AND);}
 "||"						{return TOKEN(OR);}
 "!"							{return TOKEN(NOT);}
@@ -55,11 +58,14 @@ letter        [a-zA-Z_]
 ">="						{return TOKEN(GREATEREQUAL);}
 "("							{return TOKEN(LPAREN);}
 ")"							{return TOKEN(RPAREN);}
+"["							{return TOKEN(LBRACK);}
+"]"							{return TOKEN(RBRACK);}
 "+"							{return TOKEN(PLUS);}
 "-"							{return TOKEN(MINUS);}
 "*"							{return TOKEN(MULTIPLY);}
 "="							{return TOKEN(EQUAL);}
 ":"							{return TOKEN(COLON);}
+"#"							{return TOKEN(COUNT);}
 .							{printf("Unknown token %s!\n", pqlqtext); yyterminate();}
 
 %%

diff --git a/src/PQL/SMCExpressions.cpp b/src/PQL/SMCExpressions.cpp
@@ -0,0 +1,25 @@
+#include "PQL/SMCExpressions.h"
+
+#include "PQL/Contexts.h"
+#include "PQL/Expressions.h"
+#include "errorcodes.h"
+#include "PQL/Visitor.h"
+
+namespace unfoldtacpn::PQL {
+
+    void ProbaCondition::analyze(NamingContext &context)
+    {
+        _cond->analyze(context);
+    }
+
+    void PFCondition::visit(Visitor& ctx) const
+    {
+        ctx.accept<decltype(this)>(this);
+    }
+
+    void PGCondition::visit(Visitor& ctx) const
+    {
+        ctx.accept<decltype(this)>(this);
+    }
+
+}
diff --git a/src/PQL/Visitor.cpp b/src/PQL/Visitor.cpp
@@ -24,6 +24,10 @@ namespace unfoldtacpn
             {   assert(false); std::cerr << "No accept for EUCondition" << std::endl; exit(0);}
             void Visitor::_accept(const AUCondition*)
             {   assert(false); std::cerr << "No accept for AUCondition" << std::endl; exit(0);}
+            void Visitor::_accept(const PFCondition*)
+            {   assert(false); std::cerr << "No accept for PFCondition" << std::endl; exit(0);}
+            void Visitor::_accept(const PGCondition*)
+            {   assert(false); std::cerr << "No accept for PGCondition" << std::endl; exit(0);}
 
             // shallow elements, neither of these should exist in a compiled expression
             void Visitor::_accept(const KSafeCondition* element)

diff --git a/src/PQL/XMLPrinter.cpp b/src/PQL/XMLPrinter.cpp
@@ -183,6 +183,18 @@ namespace unfoldtacpn {
             closeXmlTag("all-paths");
         }
 
+        void XMLPrinter::_accept(const PGCondition *element) {
+            openXmlTag("globally");
+            (*element)[0]->visit(*this);
+            closeXmlTag("globally");
+        }
+
+        void XMLPrinter::_accept(const PFCondition *element) {
+            openXmlTag("finally");
+            (*element)[0]->visit(*this);
+            closeXmlTag("finally");
+        }
+
         void XMLPrinter::_accept(const ControlCondition *element) {
             openXmlTag("control");
             (*element)[0]->visit(*this);
Original file line number	Diff line number	Diff line change
Expand Up		@@ -8,5 +8,5 @@ bison_target(pql_parser "${CMAKE_CURRENT_SOURCE_DIR}/PQLQueryParser.y"

		add_flex_bison_dependency(pql_lexer pql_parser)

		add_library(PQL OBJECT ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp XMLPrinter.cpp Visitor.cpp)
		add_library(PQL OBJECT ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp XMLPrinter.cpp Visitor.cpp SMCExpressions.cpp)