← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Simplification/Retval.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Simplification/Retval.h
1
 
#ifndef RETVAL_H
2
 
#define RETVAL_H
3
 
#include "LinearPrograms.h"
4
 
 
5
 
namespace PetriEngine {
6
 
    namespace Simplification {
7
 
        struct Retval {
8
 
            std::shared_ptr<PQL::Condition> formula = nullptr;
9
 
            AbstractProgramCollection_ptr lps;
10
 
            AbstractProgramCollection_ptr neglps;
11
 
            
12
 
            Retval (const std::shared_ptr<PQL::Condition> formula, 
13
 
            AbstractProgramCollection_ptr&& lps1, 
14
 
            AbstractProgramCollection_ptr&& lps2)
15
 
            : formula(formula), lps(std::move(lps1)),  neglps(std::move(lps2)) {
16
 
                assert(lps);
17
 
                assert(neglps);                
18
 
            }
19
 
 
20
 
            Retval (const std::shared_ptr<PQL::Condition> formula, 
21
 
            const AbstractProgramCollection_ptr& lps1, 
22
 
            const AbstractProgramCollection_ptr& lps2) 
23
 
            : formula(formula), lps(lps1), neglps(lps2) {
24
 
                assert(lps);
25
 
                assert(neglps);
26
 
            }
27
 
            
28
 
            Retval (const std::shared_ptr<PQL::Condition> formula) 
29
 
            : formula(formula) {
30
 
                lps = std::make_shared<SingleProgram>();
31
 
                neglps  = std::make_shared<SingleProgram>();
32
 
                assert(lps);
33
 
                assert(neglps);
34
 
            }
35
 
 
36
 
            
37
 
            Retval(const Retval&& other)
38
 
            : formula(std::move(other.formula)), lps(std::move(other.lps)), neglps(std::move(other.neglps))
39
 
            {
40
 
                assert(lps);
41
 
                assert(neglps);                
42
 
            }
43
 
            
44
 
            Retval(Retval&& other) 
45
 
            : formula(other.formula), lps(std::move(other.lps)), neglps(std::move(other.neglps))
46
 
            {
47
 
                assert(lps);
48
 
                assert(neglps);
49
 
            }
50
 
 
51
 
            Retval& operator=(Retval&& other) {
52
 
                lps = std::move(other.lps);
53
 
                neglps = std::move(other.neglps);
54
 
                formula = std::move(other.formula);
55
 
                assert(lps);
56
 
                assert(neglps);                
57
 
                return *this;
58
 
            }
59
 
            
60
 
            Retval() {
61
 
                lps = std::make_shared<SingleProgram>();
62
 
                neglps  = std::make_shared<SingleProgram>();
63
 
                assert(lps);
64
 
                assert(neglps);
65
 
            }
66
 
            
67
 
            ~Retval(){
68
 
            }
69
 
            
70
 
        private:
71
 
 
72
 
        };
73
 
    }
74
 
}
75
 
 
76
 
#endif /* RETVAL_H */
77