← Back to branch summary

~tapaal-ltl/verifypn/ltl-engine

« back to all changes in this revision

Viewing changes to src/LTL/LTLConditions.h

  • Committer: Asger Gitz-Johansen
  • Date: 2019-10-28 10:25:34 UTC
  • Revision ID: agj@hmk-t570-048-20191028102534-yjcmomlwyr3w3ekn
WIP commit. "Implemented" W/R/MCondition so they can technically be parsed.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/LTLConditions.h
8
8
//// -- It would be nice if someone would implement that though
9
9
////
10
10
//// NOTE: The "implementations" are just place holders so the classes can be instantiated.
 
11
////       They are NOT tested with the rest of the verifypn query framework.
11
12
 
12
13
namespace PetriEngine::PQL {
13
14
        
16
17
    public:
17
18
            XCondition(Condition_ptr& p) : SimpleQuantifierCondition(p) {}
18
19
        uint32_t distance(DistanceContext& context) const override { return 0; }
19
 
        Retval simplify(SimplificationContext& context) const override { return Simplification::Retval(); }
 
20
        Retval simplify(SimplificationContext& context) const override { return Simplification::Retval(); } // TODO: This should be implemented. As a start, LTL properties just cannot be simplified at all.
20
21
        bool isReachability(uint32_t depth) const override { return false; }
21
22
        Condition_ptr prepareForReachability(bool negated) const override { return std::shared_ptr<Condition>(); }
22
 
        Condition_ptr pushNegation(negstat_t& negstat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override { return std::shared_ptr<Condition>(); }
 
23
        Condition_ptr pushNegation(negstat_t& negstat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override { return std::shared_ptr<Condition>(); } // TODO: This should be implemented. Otherwise the main file _can_ break this.
23
24
        void toXML(std::ostream& ostream1, uint32_t tabs) const override {}
24
25
        Quantifier getQuantifier() const override { return EMPTY; }
25
26
        Path getPath() const override { return X; }
75
76
    };
76
77
        // LTL Weak until
77
78
        class WCondition : public UntilCondition, public Condition_RuntimeType<WCondition> {
 
79
        public:
 
80
                WCondition(Condition_ptr& a, Condition_ptr& b) : UntilCondition(a,b) {}
 
81
                uint32_t distance(DistanceContext& context) const override { return 0; }
 
82
                Retval simplify(SimplificationContext& context) const override { return Simplification::Retval(); }
 
83
                Condition_ptr prepareForReachability(bool negated) const override { return std::shared_ptr<Condition>(); }
 
84
                Condition_ptr  pushNegation(negstat_t& negstat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override { return std::shared_ptr<Condition>(); }
 
85
                void toXML(std::ostream& ostream1, uint32_t tabs) const override {}
 
86
                Quantifier getQuantifier() const override { return EMPTY; }
78
87
        
 
88
        private:
 
89
                string op() const override { return std::__cxx11::string(); }
79
90
        };
80
91
        // LTL Release
81
92
        class RCondition : public UntilCondition, public Condition_RuntimeType<RCondition> {
 
93
        public:
 
94
                RCondition(Condition_ptr& a, Condition_ptr& b) : UntilCondition(a,b) {}
 
95
                uint32_t distance(DistanceContext& context) const override { return 0; }
 
96
                Retval simplify(SimplificationContext& context) const override { return Simplification::Retval(); }
 
97
                Condition_ptr prepareForReachability(bool negated) const override { return std::shared_ptr<Condition>(); }
 
98
                Condition_ptr  pushNegation(negstat_t& negstat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override { return std::shared_ptr<Condition>(); }
 
99
                void toXML(std::ostream& ostream1, uint32_t tabs) const override {}
 
100
                Quantifier getQuantifier() const override { return EMPTY; }
82
101
        
 
102
        private:
 
103
                string op() const override { return std::__cxx11::string(); }
83
104
        };
84
105
        // LTL Strong release (M)
85
106
        class MCondition : public UntilCondition, public Condition_RuntimeType<MCondition> {
 
107
        public:
 
108
                MCondition(Condition_ptr& a, Condition_ptr& b) : UntilCondition(a,b) {}
 
109
                uint32_t distance(DistanceContext& context) const override { return 0; }
 
110
                Retval simplify(SimplificationContext& context) const override { return Simplification::Retval(); }
 
111
                Condition_ptr prepareForReachability(bool negated) const override { return std::shared_ptr<Condition>(); }
 
112
                Condition_ptr  pushNegation(negstat_t& negstat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override { return std::shared_ptr<Condition>(); }
 
113
                void toXML(std::ostream& ostream1, uint32_t tabs) const override {}
 
114
                Quantifier getQuantifier() const override { return EMPTY; }
86
115
        
 
116
        private:
 
117
                string op() const override { return std::__cxx11::string(); }
87
118
        };
88
119
        
89
120
}