← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/CTL/SearchStrategy/SearchStrategy.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:
include/CTL/SearchStrategy/SearchStrategy.h
 
1
#ifndef ISEARCHSTRATEGY_H
 
2
#define ISEARCHSTRATEGY_H
 
3
 
 
4
#include "CTL/DependencyGraph/Edge.h"
 
5
#include <sstream>
 
6
 
 
7
namespace SearchStrategy {
 
8
 
 
9
struct Message {    
 
10
    uint32_t sender;
 
11
    uint32_t distance;
 
12
    enum Type {HALT = 0, REQUEST = 1, ANSWER_ONE = 2, ANSWER_ZERO = 3} type;
 
13
    DependencyGraph::Configuration *configuration;
 
14
 
 
15
    Message() {}
 
16
    Message(size_t sender, uint32_t distance, Type type, DependencyGraph::Configuration *configuration) :
 
17
           sender(sender), distance(distance), type(type), configuration(configuration) {}
 
18
 
 
19
    std::string ToString() {
 
20
        std::stringstream ss;
 
21
        ss << "Message from " << sender << ": ";
 
22
        ss << (type == HALT ? "Halt" : type == REQUEST ? "Request" : type == ANSWER_ONE ? "Answer 1" : "Answer 0");
 
23
        ss << configuration << "\n";
 
24
        return ss.str();
 
25
    }
 
26
};
 
27
 
 
28
 
 
29
class SearchStrategy
 
30
{
 
31
public:
 
32
    virtual ~SearchStrategy() {};
 
33
    bool empty() const;
 
34
    void pushEdge(DependencyGraph::Edge *edge);
 
35
    void pushDependency(DependencyGraph::Edge* edge);
 
36
    void pushNegation(DependencyGraph::Edge *edge);
 
37
    DependencyGraph::Edge* popEdge(bool saturate = false);
 
38
    size_t size() const;
 
39
//#ifdef VERIFYPNDIST
 
40
    uint32_t maxDistance() const;
 
41
    bool available() const;
 
42
    void releaseNegationEdges(uint32_t );
 
43
    bool trivialNegation();
 
44
    virtual void flush() {};
 
45
//#endif
 
46
protected:
 
47
    virtual size_t Wsize() const = 0;
 
48
    virtual void pushToW(DependencyGraph::Edge* edge) = 0;
 
49
    virtual DependencyGraph::Edge* popFromW() = 0;
 
50
    
 
51
    std::vector<DependencyGraph::Edge*> N;
 
52
    std::vector<DependencyGraph::Edge*> D;
 
53
};
 
54
 
 
55
}
 
56
#endif // SEARCHSTRATEGY_H