← Back to branch summary

~verifypn-cpn/verifypn/RERS_2018

« back to all changes in this revision

Viewing changes to PetriEngine/PQL/Expressions.cpp

  • Committer: Peter G. Jensen
  • Date: 2018-10-04 17:48:09 UTC
  • Revision ID: peter.gjoel@gmail.com-20181004174809-xrlpv9pb37x3kh2s
should parse RERS ctl-semantics, reductions might be incorrect

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/PQL/Expressions.cpp
2145
2145
            // we could technically also check some LP's here to see if we
2146
2146
            // can show that NO transition can ever be enabled; implying true.
2147
2147
            // otherwise we can remove non-enableable transitions
2148
 
            /*if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
2149
 
                // we cannot unfold in the same way as the ETCondition as we have
2150
 
                // an extra clause that it is ONLY for enabled transitions (not all)
2151
 
                return std::make_shared<UnfoldedFireableCondition>(transname);
2152
 
            } else*/
2153
 
            /*if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {
 
2148
            if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {
2154
2149
                return Retval(BooleanCondition::TRUE_CONSTANT);                
2155
 
            } else*/ {
 
2150
            } else {
2156
2151
                return Retval(std::make_shared<ATransitionCondition>(transname, r.formula, trans));
2157
2152
            }
2158
2153
        }
2163
2158
            // can show that NO transition can ever be enabled; implying false.
2164
2159
            // otherwise we can remove non-enableable transitions
2165
2160
            assert(trans.size() > 0);
2166
 
            /*if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
2167
 
                return Retval(BooleanCondition::FALSE_CONSTANT);                        
2168
 
            } else*/ if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {
2169
 
                std::vector<Condition_ptr> unfolded;
2170
 
                for(auto t : trans)
2171
 
                {
2172
 
                    std::vector<Condition_ptr> to_fire;
2173
 
                    auto pre = context.net()->preset(t);
2174
 
                    for(;pre.first != pre.second; ++pre.first)
2175
 
                    {
2176
 
                        auto& inv = *pre.first;
2177
 
                        auto lit = std::make_shared<LiteralExpr>(inv.tokens);
2178
 
                        auto place = std::make_shared<UnfoldedIdentifierExpr>(context.net()->placeNames()[inv.place], inv.place);
2179
 
                        if(inv.inhibitor)
2180
 
                            to_fire.emplace_back(std::make_shared<LessThanCondition>(lit, place));
2181
 
                        else
2182
 
                            to_fire.emplace_back(std::make_shared<GreaterThanOrEqualCondition>(lit, place));                        
2183
 
                    }
2184
 
                    unfolded.emplace_back(std::make_shared<AndCondition>(std::move(to_fire)));
2185
 
                }
2186
 
                return OrCondition(std::move(unfolded)).simplify(context);
 
2161
            if(r.formula->isTriviallyFalse() || !r.lps->satisfiable(context)){
 
2162
                return Retval(BooleanCondition::FALSE_CONSTANT);                                        
2187
2163
            } else {
2188
2164
                return Retval(std::make_shared<ETransitionCondition>(transname, r.formula, trans));
2189
2165
            }
3125
3101
            auto a = _cond->pushNegation(stats, context, true, false, initrw);
3126
3102
            if(a == BooleanCondition::TRUE_CONSTANT)
3127
3103
                return a;
 
3104
            else if (a == BooleanCondition::FALSE_CONSTANT)
 
3105
            {
 
3106
                std::vector<Condition_ptr> unfolded;
 
3107
                for(auto t : _transitions)
 
3108
                {
 
3109
                    std::vector<Condition_ptr> to_fire;
 
3110
                    auto pre = context.net()->preset(t);
 
3111
                    for(;pre.first != pre.second; ++pre.first)
 
3112
                    {
 
3113
                        auto& inv = *pre.first;
 
3114
                        auto lit = std::make_shared<LiteralExpr>(inv.tokens);
 
3115
                        auto place = std::make_shared<UnfoldedIdentifierExpr>(context.net()->placeNames()[inv.place], inv.place);
 
3116
                        if(inv.inhibitor)
 
3117
                            to_fire.emplace_back(std::make_shared<LessThanCondition>(lit, place));
 
3118
                        else
 
3119
                            to_fire.emplace_back(std::make_shared<GreaterThanOrEqualCondition>(lit, place));                        
 
3120
                    }
 
3121
                    unfolded.emplace_back(std::make_shared<NotCondition>(std::make_shared<AndCondition>(std::move(to_fire))));
 
3122
                }
 
3123
                return AndCondition(std::move(unfolded)).pushNegation(stats, context, nested, negated, initrw); 
 
3124
            }
3128
3125
            if(negated)
3129
3126
                return ETransitionCondition(_transname, std::make_shared<NotCondition>(a), _transitions).pushNegation(stats, context, nested, false, initrw);
3130
3127
            else
3136
3133
            auto a = _cond->pushNegation(stats, context, true, false, initrw);
3137
3134
            if(a == BooleanCondition::FALSE_CONSTANT)
3138
3135
                return a;
 
3136
            else if(a == BooleanCondition::TRUE_CONSTANT)
 
3137
            {
 
3138
                std::vector<Condition_ptr> unfolded;
 
3139
                for(auto t : _transitions)
 
3140
                {
 
3141
                    std::vector<Condition_ptr> to_fire;
 
3142
                    auto pre = context.net()->preset(t);
 
3143
                    for(;pre.first != pre.second; ++pre.first)
 
3144
                    {
 
3145
                        auto& inv = *pre.first;
 
3146
                        auto lit = std::make_shared<LiteralExpr>(inv.tokens);
 
3147
                        auto place = std::make_shared<UnfoldedIdentifierExpr>(context.net()->placeNames()[inv.place], inv.place);
 
3148
                        if(inv.inhibitor)
 
3149
                            to_fire.emplace_back(std::make_shared<LessThanCondition>(lit, place));
 
3150
                        else
 
3151
                            to_fire.emplace_back(std::make_shared<GreaterThanOrEqualCondition>(lit, place));                        
 
3152
                    }
 
3153
                    unfolded.emplace_back(std::make_shared<AndCondition>(std::move(to_fire)));
 
3154
                }
 
3155
                return OrCondition(std::move(unfolded)).pushNegation(stats, context, nested, negated, initrw);                
 
3156
            }
3139
3157
            if(negated)
3140
3158
                return ATransitionCondition(_transname, std::make_shared<NotCondition>(a), _transitions).pushNegation(stats, context, nested, false, initrw);
3141
3159
            else