diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml
index 52b27df..6851c46 100644
--- 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
index 877fb33..a012950 100644
--- 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
index 6ad0b12..7989001 100644
--- 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
new file mode 100644
index 0000000..fe18d28
--- /dev/null
+++ 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
\ No newline at end of file
diff --git a/include/PQL/Visitor.h b/include/PQL/Visitor.h
index f65407d..145f4d1 100644
--- 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
index 6e9496c..1de9c0e 100644
--- 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
index 14da177..bf2dd64 100644
--- 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
index 66afefd..3f10f09 100644
--- 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
index 7f3b72f..e5523fc 100644
--- 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
index bb1c258..ef7a4b3 100644
--- 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
index 7e86b51..cc6c54e 100644
--- 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
index bd6fe84..b43d176 100644
--- 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
index 448ab0b..e90a5ce 100644
--- 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
index 84790c2..d48adc1 100644
--- 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; }
-		;
+		;
\ No newline at end of file
diff --git a/src/PQL/PQLQueryTokens.l b/src/PQL/PQLQueryTokens.l
index 0b17e8c..a604fef 100644
--- 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
new file mode 100644
index 0000000..9fbbc21
--- /dev/null
+++ 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);
+    }
+
+}
\ No newline at end of file
diff --git a/src/PQL/Visitor.cpp b/src/PQL/Visitor.cpp
index 227fdae..e86e301 100644
--- 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
index bd94237..d97b7dd 100644
--- 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);
diff --git a/src/PetriParse/PNMLParser.cpp b/src/PetriParse/PNMLParser.cpp
index ef584fb..6413c18 100644
--- a/src/PetriParse/PNMLParser.cpp
+++ b/src/PetriParse/PNMLParser.cpp
@@ -773,6 +773,10 @@ void PNMLParser::parseTransition(rapidxml::xml_node<>* element) {
     int player = 0;
     unfoldtacpn::Colored::GuardExpression_ptr expr = nullptr;
     auto name = element->first_attribute("id")->value();
+    Colored::SMC::Distribution distrib = Colored::SMC::Constant;
+    Colored::SMC::DistributionParameters distrib_params = { 1.0, 0.0 };
+    double weight = 1.0;
+    Colored::SMC::FiringMode firingMode = Colored::SMC::Oldest;
 
     auto posX = element->first_attribute("positionX");
     if (posX != nullptr){
@@ -792,6 +796,29 @@ void PNMLParser::parseTransition(rapidxml::xml_node<>* element) {
         player = atoi(pl_el->value());
     }
 
+    if(!urgent) {
+        auto dist_data = parseDistribution(element);
+        distrib = std::get<0>(dist_data);
+        distrib_params = std::get<1>(dist_data);
+    } else if(urgent) {
+        distrib_params.param1 = 0;
+    }
+
+    auto weight_el = element->first_attribute("weight");
+    if(weight_el != nullptr) {
+        weight = atof(weight_el->value());
+    }
+
+    auto firing_el = element->first_attribute("firingMode");
+    if(firing_el != nullptr) {
+        if (strcasecmp(firing_el->value(), "oldest") == 0) {
+            firingMode = Colored::SMC::Oldest;
+        } else if (strcasecmp(firing_el->value(), "youngest") == 0) {
+            firingMode = Colored::SMC::Youngest;
+        } else if (strcasecmp(firing_el->value(), "random") == 0) {
+            firingMode = Colored::SMC::Random;
+        } 
+    }
 
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
         if (strcmp(it->name(), "graphics") == 0) {
@@ -806,7 +833,47 @@ void PNMLParser::parseTransition(rapidxml::xml_node<>* element) {
             exit(ErrorCode);
         }
     }
-    _builder->addTransition(name, expr, player, urgent, x, y);
+    _builder->addTransition(name, expr, player, urgent, x, y, distrib, distrib_params, weight, firingMode);
+}
+
+std::tuple<Colored::SMC::Distribution, Colored::SMC::DistributionParameters> PNMLParser::parseDistribution(rapidxml::xml_node<>* element) {
+    Colored::SMC::Distribution distrib = Colored::SMC::Constant;
+    Colored::SMC::DistributionParameters distrib_params = { 1.0, 0.0 };
+    auto distrib_el = element->first_attribute("distribution");
+    if(distrib_el != nullptr) {
+        char* distrib_name = distrib_el->value();
+        if(strcasecmp(distrib_name, "constant") == 0) {
+            distrib = Colored::SMC::Constant;
+            distrib_params.param1 = atof(element->first_attribute("value")->value());
+        } else if(strcasecmp(distrib_name, "uniform") == 0) {
+            distrib = Colored::SMC::Uniform;
+            distrib_params.param1 = atof(element->first_attribute("a")->value());
+            distrib_params.param2 = atof(element->first_attribute("b")->value());
+        } else if(strcasecmp(distrib_name, "exponential") == 0) {
+            distrib = Colored::SMC::Exponential;
+            distrib_params.param1 = atof(element->first_attribute("rate")->value());
+        } else if(strcasecmp(distrib_name, "normal") == 0) {
+            distrib = Colored::SMC::Normal;
+            distrib_params.param1 = atof(element->first_attribute("mean")->value());
+            distrib_params.param2 = atof(element->first_attribute("stddev")->value());
+        } else if(strcasecmp(distrib_name, "gamma") == 0) {
+            distrib = Colored::SMC::Gamma;
+            distrib_params.param1 = atof(element->first_attribute("shape")->value());
+            distrib_params.param2 = atof(element->first_attribute("scale")->value());
+        } else if(strcasecmp(distrib_name, "erlang") == 0) {
+            distrib = Colored::SMC::Erlang;
+            distrib_params.param1 = atof(element->first_attribute("shape")->value());
+            distrib_params.param2 = atof(element->first_attribute("scale")->value());
+        } else if(strcasecmp(distrib_name, "discrete uniform") == 0) {
+            distrib = Colored::SMC::DiscreteUniform;
+            distrib_params.param1 = atof(element->first_attribute("a")->value());
+            distrib_params.param2 = atof(element->first_attribute("b")->value());
+        } else if(strcasecmp(distrib_name, "geometric") == 0) {
+            distrib = Colored::SMC::Geometric;
+            distrib_params.param1 = atof(element->first_attribute("p")->value());
+        }
+    }
+    return std::make_pair(distrib, distrib_params);
 }
 
 void PNMLParser::parseValue(rapidxml::xml_node<>* element, std::string& text) {
diff --git a/src/PetriParse/QueryXMLParser.cpp b/src/PetriParse/QueryXMLParser.cpp
index 2bdfeb1..bfcae74 100644
--- a/src/PetriParse/QueryXMLParser.cpp
+++ b/src/PetriParse/QueryXMLParser.cpp
@@ -18,6 +18,7 @@
 
 #include "PetriParse/QueryXMLParser.h"
 #include "PQL/Expressions.h"
+#include "PQL/SMCExpressions.h"
 #include "errorcodes.h"
 
 #include <string>
@@ -94,6 +95,7 @@ bool QueryXMLParser::parseProperty(rapidxml::xml_node<>*  element) {
     string id;
     bool tagsOK = true;
     rapidxml::xml_node<>* formulaPtr = nullptr;
+    rapidxml::xml_node<>* smcPtr = nullptr;
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
         if (strcmp(it->name(), "id") == 0) {
             id = it->value();
@@ -101,6 +103,8 @@ bool QueryXMLParser::parseProperty(rapidxml::xml_node<>*  element) {
             formulaPtr = it;
         } else if (strcmp(it->name(), "tags") == 0) {
             tagsOK = parseTags(it);
+        } else if (strcmp(it->name(), "smc") == 0) {
+            smcPtr = it;
         }
     }
 
@@ -111,11 +115,15 @@ bool QueryXMLParser::parseProperty(rapidxml::xml_node<>*  element) {
 
     QueryItem queryItem;
     queryItem.id = id;
-    if(tagsOK)
-    {
+    if(tagsOK && smcPtr == nullptr) {
         queryItem.query = parseFormula(formulaPtr);
         assert(queryItem.query);
         queryItem.parsingResult = QueryItem::PARSING_OK;
+    } else if(tagsOK && smcPtr != nullptr) {
+        SMCSettings settings = parseSmcSettings(smcPtr);
+        queryItem.query = parseSmcFormula(settings, formulaPtr);
+        assert(queryItem.query);
+        queryItem.parsingResult = QueryItem::PARSING_OK;
     } else {
         queryItem.query = nullptr;
         queryItem.parsingResult = QueryItem::UNSUPPORTED_QUERY;
@@ -450,6 +458,72 @@ Condition_ptr QueryXMLParser::parseBooleanFormula(rapidxml::xml_node<>*  element
     return nullptr;
 }
 
+SMCSettings QueryXMLParser::parseSmcSettings(rapidxml::xml_node<>* smcNode) {
+    SMCSettings settings {
+        std::numeric_limits<int>::max(), std::numeric_limits<int>::max(),
+        0.05f, 0.05f,
+        0.05f, 0.05f,
+        0.95f, 0.05f,
+        false, 0.0f,
+    };
+    auto timeBound = smcNode->first_attribute("time-bound");
+    if(timeBound != nullptr)
+        settings.timeBound = atoi(timeBound->value());
+    auto stepBound = smcNode->first_attribute("step-bound");
+    if(stepBound != nullptr)
+        settings.stepBound = atoi(stepBound->value());
+    auto falsePos = smcNode->first_attribute("false-positives");
+    if(falsePos != nullptr)
+        settings.falsePositives = atof(falsePos->value());
+    auto falseNeg = smcNode->first_attribute("false-negatives");
+    if(falseNeg != nullptr)
+        settings.falseNegatives = atof(falseNeg->value());
+    auto indifference = smcNode->first_attribute("indifference");
+    if(indifference != nullptr) {
+        settings.indifferenceRegionDown = atof(indifference->value());
+        settings.indifferenceRegionUp = atof(indifference->value());
+    }
+    auto confidence = smcNode->first_attribute("confidence");
+    if(confidence != nullptr)
+        settings.confidence = atof(confidence->value());
+    auto intervalWidth = smcNode->first_attribute("interval-width");
+    if(intervalWidth != nullptr) 
+        settings.estimationIntervalWidth = atof(intervalWidth->value());
+    auto compareToF = smcNode->first_attribute("compare-to");
+    if(compareToF != nullptr) {
+        settings.compareToFloat = true;
+        settings.geqThan = atof(compareToF->value());
+    }
+    return settings;
+}
+
+Condition_ptr QueryXMLParser::parseSmcFormula(SMCSettings settings, rapidxml::xml_node<>* element) {
+    if (getChildCount(element) != 1) {
+        assert(false);
+        return nullptr;
+    }
+    auto child = element->first_node();
+    string childName = child->name();
+    Condition_ptr cond = nullptr;
+    if(childName == "finally") {
+        if (getChildCount(child) != 1) {
+            assert(false);
+            return nullptr;
+        }
+        if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
+            return std::make_shared<PFCondition>(settings, cond);
+    } else if(childName == "globally") {
+        if (getChildCount(child) != 1) {
+            assert(false);
+            return nullptr;
+        }
+        if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
+            return std::make_shared<PGCondition>(settings, cond);
+    }
+    assert(false);
+    return nullptr;
+}
+
 Expr_ptr QueryXMLParser::parseIntegerExpression(rapidxml::xml_node<>*  element) {
     string elementName = element->name();
     if (elementName == "integer-constant") {