← Back to branch summary

~tapaal-contributor/verifypn/show-reduced-net

« back to all changes in this revision

Viewing changes to CTL/CTLEngine.cpp

  • 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:
CTL/CTLEngine.cpp
1
 
#include "CTLEngine.h"
2
 
 
3
 
#include "PetriNets/OnTheFlyDG.h"
4
 
#include "CTLResult.h"
5
 
#include "DependencyGraph/Edge.h"
6
 
 
7
 
#include "SearchStrategy/DFSSearch.h"
8
 
 
9
 
#include "Algorithm/CertainZeroFPA.h"
10
 
#include "Algorithm/LocalFPA.h"
11
 
 
12
 
#include "PetriEngine/PQL/PQL.h"
13
 
 
14
 
#include "Stopwatch.h"
15
 
#include "PetriEngine/options.h"
16
 
#include "CTL/Algorithm/AlgorithmTypes.h"
17
 
 
18
 
#include <iostream>
19
 
#include <iomanip>
20
 
#include <fstream>
21
 
#include <sstream>
22
 
#include <vector>
23
 
 
24
 
using namespace std;
25
 
using namespace PetriEngine::PQL;
26
 
 
27
 
 
28
 
ReturnValue getAlgorithm(std::shared_ptr<Algorithm::FixedPointAlgorithm>& algorithm,
29
 
                         CTL::CTLAlgorithmType algorithmtype, PetriEngine::Reachability::Strategy search)
30
 
{
31
 
    switch(algorithmtype)
32
 
    {
33
 
        case CTL::CTLAlgorithmType::Local:
34
 
            algorithm = std::make_shared<Algorithm::LocalFPA>(search);
35
 
            break;
36
 
        case CTL::CTLAlgorithmType::CZero:
37
 
            algorithm = std::make_shared<Algorithm::CertainZeroFPA>(search);
38
 
            break;
39
 
        default:
40
 
            cerr << "Error: Unknown or unsupported algorithm" << endl;
41
 
            return ErrorCode;
42
 
    }
43
 
    return ContinueCode;
44
 
}
45
 
 
46
 
void printResult(const std::string& qname, CTLResult& result, bool statisticslevel, bool mccouput, bool only_stats, size_t index, options_t& options){
47
 
    const static string techniques = "TECHNIQUES COLLATERAL_PROCESSING EXPLICIT STATE_COMPRESSION SAT_SMT ";
48
 
 
49
 
    if(!only_stats)
50
 
    {
51
 
        cout << endl;
52
 
        cout << "FORMULA "
53
 
             << qname
54
 
             << " " << (result.result ? "TRUE" : "FALSE") << " "
55
 
             << techniques
56
 
             << (options.isCPN ? "UNFOLDING_TO_PT " : "")
57
 
             << (options.stubbornreduction ? "STUBBORN_SETS " : "")
58
 
             << (options.ctlalgorithm == CTL::CZero ? "CTL_CZERO " : "")
59
 
             << (options.ctlalgorithm == CTL::Local ? "CTL_LOCAL " : "")
60
 
                << endl << endl;
61
 
        std::cout << "Query index " << index << " was solved" << std::endl;
62
 
        cout << "Query is" << (result.result ? "" : " NOT") << " satisfied." << endl;
63
 
 
64
 
        cout << endl;
65
 
    }
66
 
    if(statisticslevel){
67
 
        cout << "STATS:" << endl;
68
 
        cout << "       Time (seconds)    : " << setprecision(4) << result.duration / 1000 << endl;
69
 
        cout << "       Configurations    : " << result.numberOfConfigurations << endl;
70
 
        cout << "       Markings          : " << result.numberOfMarkings << endl;
71
 
        cout << "       Edges             : " << result.numberOfEdges << endl;
72
 
        cout << "       Processed Edges   : " << result.processedEdges << endl;
73
 
        cout << "       Processed N. Edges: " << result.processedNegationEdges << endl;
74
 
        cout << "       Explored Configs  : " << result.exploredConfigurations << endl;
75
 
        std::cout << endl;
76
 
    }
77
 
}
78
 
 
79
 
ReturnValue CTLMain(PetriEngine::PetriNet* net,
80
 
                    CTL::CTLAlgorithmType algorithmtype,
81
 
                    PetriEngine::Reachability::Strategy strategytype,
82
 
                    bool gamemode,
83
 
                    bool printstatistics,
84
 
                    bool mccoutput,
85
 
                    bool partial_order,
86
 
                    const std::vector<std::string>& querynames,
87
 
                    const std::vector<std::shared_ptr<Condition>>& queries,
88
 
                    const std::vector<size_t>& querynumbers,
89
 
                    options_t& options
90
 
        )
91
 
{
92
 
 
93
 
    for(auto qnum : querynumbers){
94
 
        CTLResult result(queries[qnum]);
95
 
        PetriNets::OnTheFlyDG graph(net, partial_order); 
96
 
        graph.setQuery(result.query);
97
 
        std::shared_ptr<Algorithm::FixedPointAlgorithm> alg = nullptr;
98
 
        bool solved = false;
99
 
        switch(graph.initialEval())
100
 
        {
101
 
            case Condition::Result::RFALSE:
102
 
                result.result = false;
103
 
                solved = true;
104
 
                break;
105
 
            case Condition::Result::RTRUE:
106
 
                result.result = true;
107
 
                solved = true;
108
 
                break;
109
 
            default:
110
 
                break;
111
 
        }
112
 
        
113
 
        if(!solved)
114
 
        {            
115
 
            if(getAlgorithm(alg, algorithmtype,  strategytype) == ErrorCode)
116
 
            {
117
 
                return ErrorCode;
118
 
            }
119
 
 
120
 
            stopwatch timer;
121
 
            timer.start();
122
 
            result.result = alg->search(graph);
123
 
            timer.stop();
124
 
 
125
 
            result.duration = timer.duration();
126
 
        }
127
 
        result.numberOfConfigurations = graph.configurationCount();
128
 
        result.numberOfMarkings = graph.markingCount();
129
 
        result.processedEdges = alg ? alg->processedEdges() : 0;
130
 
        result.processedNegationEdges = alg ? alg->processedNegationEdges() : 0;
131
 
        result.exploredConfigurations = alg ? alg->exploredConfigurations() : 0;
132
 
        result.numberOfEdges = alg ? alg->numberOfEdges() : 0;
133
 
        printResult(querynames[qnum], result, printstatistics, mccoutput, false, qnum, options);
134
 
    }
135
 
    return SuccessCode;
136
 
}