← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/STSolver.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/STSolver.h
1
 
#ifndef STSOLVER_H
2
 
#define STSOLVER_H
3
 
#include "Structures/State.h"
4
 
#include "../lpsolve/lp_lib.h"
5
 
#include "Reachability/ReachabilityResult.h"
6
 
#include <memory>
7
 
#include <chrono>
8
 
 
9
 
namespace PetriEngine {
10
 
    class STSolver {
11
 
    
12
 
    struct STVariable {
13
 
        STVariable(int c, REAL v){
14
 
            colno=c;
15
 
            value=v;
16
 
        }
17
 
        int colno;
18
 
        REAL value;
19
 
    };
20
 
    
21
 
    struct place_t {
22
 
        uint32_t pre, post;
23
 
    };
24
 
        
25
 
    public:
26
 
        STSolver(Reachability::ResultPrinter& printer, const PetriNet& net, PQL::Condition * query, uint32_t depth);
27
 
        virtual ~STSolver();
28
 
        int CreateFormula();
29
 
        int Solve(uint32_t timeout);
30
 
        void PrintStatistics();
31
 
        Reachability::ResultPrinter::Result PrintResult();
32
 
        int getResult(){
33
 
            return _ret;
34
 
        }
35
 
        uint32_t getAnalysisTime(){
36
 
            return _analysisTime;
37
 
        }
38
 
        
39
 
    private:        
40
 
        std::string VarName(uint32_t index);
41
 
        void MakeConstraint(std::vector<STVariable> constraint, int constr_type, REAL rh);
42
 
        int CreateSiphonConstraints();
43
 
        int CreateStepConstraints(uint32_t i);
44
 
        int CreatePostVarDefinitions(uint32_t i);
45
 
        int CreateNoTrapConstraints();
46
 
        void constructPrePost();
47
 
        uint32_t duration() const;
48
 
        bool timeout() const;
49
 
        
50
 
        Reachability::ResultPrinter& printer;
51
 
        PQL::Condition * _query;
52
 
        std::unique_ptr<place_t[]> _places;
53
 
        std::unique_ptr<uint32_t> _transitions;
54
 
        const PetriNet& _net;
55
 
        const MarkVal* _m0;
56
 
        lprec* _lp;
57
 
        uint32_t _siphonDepth;
58
 
        uint32_t _nPlaceVariables;
59
 
        uint32_t _nCol;
60
 
        int _ret = 0;     
61
 
        uint32_t _timelimit;
62
 
        uint32_t _analysisTime;
63
 
        int _buildTime;
64
 
        bool _lpBuilt;
65
 
        bool _solved;
66
 
        int _noTrap = 0;
67
 
        std::chrono::high_resolution_clock::time_point _start;
68
 
    };
69
 
}
70
 
#endif /* STSOLVER_H */
71