← Back to branch summary

~tapaal-ltl/verifypn/loopInvariantReduction

« back to all changes in this revision

Viewing changes to src/LTL/LTLMain.cpp

  • Committer: Simon Virenfeldt
  • Date: 2021-02-15 14:07:35 UTC
  • Revision ID: simwir1@gmail.com-20210215140735-qzy97lpbh9v7mx8y
Implemented is dirty. Corectness testing begun

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/LTLMain.cpp
31
31
        bool satisfied = false;
32
32
        bool is_weak = true;
33
33
        Algorithm algorithm = Algorithm::Tarjan;
 
34
        bool loopInvariantReduction = false;
34
35
    };
35
36
 
36
37
/**
60
61
        return std::make_pair(converted, should_negate);
61
62
    }
62
63
 
 
64
    void printStats(PetriNetBuilder& builder, options_t& options)
 
65
    {
 
66
        if (options.printstatistics) {
 
67
            if (options.enablereduction != 0) {
 
68
 
 
69
                std::cout << "Size of net before structural reductions: " <<
 
70
                          builder.numberOfPlaces() << " places, " <<
 
71
                          builder.numberOfTransitions() << " transitions" << std::endl;
 
72
                std::cout << "Size of net after structural reductions: " <<
 
73
                          builder.numberOfPlaces() - builder.RemovedPlaces() << " places, " <<
 
74
                          builder.numberOfTransitions() - builder.RemovedTransitions() << " transitions" << std::endl;
 
75
                std::cout << "Structural reduction finished after " << builder.getReductionTime() <<
 
76
                          " seconds" << std::endl;
 
77
 
 
78
                std::cout   << "\nNet reduction is enabled.\n";
 
79
                builder.printStats(std::cout);
 
80
            }
 
81
        }
 
82
    }
 
83
 
63
84
    void reduce(Condition_ptr &negatedQuery, PetriEngine::PetriNetBuilder &builder,
64
85
                options_t &options, bool removeLoops) {
65
86
        QueryPlaceAnalysisContext placecontext(builder.getPlaceNames(), builder.getTransitionNames(), nullptr);
70
91
                                     false, containsNext, options.reductions);
71
92
    }
72
93
 
 
94
#define PRINTFDEBUG
 
95
 
73
96
    template<typename Checker>
74
97
    Result
75
98
    _verify(Condition_ptr &negatedQuery, bool printstats, options_t &options, PetriEngine::PetriNetBuilder &builder) {
76
99
        Result result;
77
100
        if (options.enablereduction > 0) {
 
101
            PetriNetBuilder loopInvariantBuilder(builder);
78
102
            bool conclusive_answer = false;
79
 
            reduce(negatedQuery, builder, options, true);
80
 
            auto modelChecker = std::make_unique<Checker>(*builder.makePetriNet(), negatedQuery);
 
103
            reduce(negatedQuery, loopInvariantBuilder, options, true);
 
104
            printStats(loopInvariantBuilder, options);
 
105
            auto net = std::unique_ptr<PetriNet>{loopInvariantBuilder.makePetriNet()};
 
106
            if(!options.model_out_file.empty())
 
107
            {
 
108
                fstream file;
 
109
                file.open(options.model_out_file, std::ios::out);
 
110
                net->toXML(file);
 
111
            }
 
112
            auto modelChecker = std::make_unique<Checker>(*net, negatedQuery);
81
113
            bool satisfied = modelChecker->isSatisfied();
82
 
            if (satisfied) {
 
114
            if (!satisfied) {
 
115
                result.satisfied = false;
 
116
                conclusive_answer = true;
 
117
#ifdef PRINTFDEBUG
 
118
                std::cerr << "Conclusive negative answer" << std::endl;
 
119
#endif
 
120
            } else if (!modelChecker->isReductionDirty() || !loopInvariantBuilder.getReducer()->loopRemovalApplied()) {
83
121
                result.satisfied = true;
84
122
                conclusive_answer = true;
85
 
            } else if (!modelChecker->isDirty()) {
86
 
                result.satisfied = false;
87
 
                conclusive_answer = true;
 
123
#ifdef PRINTFDEBUG
 
124
                if (loopInvariantBuilder.getReducer()->loopRemovalApplied())
 
125
                    std::cerr << "Conclusive positive answer" << std::endl;
 
126
                else
 
127
                    std::cerr << "No loop removal applied. So positive answer is conclusive.";
 
128
#endif
88
129
            }
89
130
            result.is_weak = modelChecker->isweak();
90
131
            if (conclusive_answer) {
91
132
                if (printstats) {
92
133
                    modelChecker->printStats(std::cout);
93
134
                }
 
135
                result.loopInvariantReduction = loopInvariantBuilder.getReducer()->loopRemovalApplied();
94
136
                return result;
95
137
            }
96
138
        }
 
139
        if (options.enablereduction > 0) {
97
140
            reduce(negatedQuery, builder, options, false);
98
 
            auto modelChecker = std::make_unique<Checker>(*builder.makePetriNet(), negatedQuery);
99
 
            result.satisfied = modelChecker->isSatisfied();
100
 
            result.is_weak = modelChecker->isweak();
 
141
            printStats(builder, options);
 
142
        }
 
143
        auto modelChecker = std::make_unique<Checker>(*builder.makePetriNet(), negatedQuery);
 
144
        result.satisfied = modelChecker->isSatisfied();
 
145
        result.is_weak = modelChecker->isweak();
 
146
#ifdef PRINTFDEBUG
 
147
        std::cerr << "Loop sensitive reduction answer" << std::endl;
 
148
#endif
101
149
        if (printstats) {
102
150
            modelChecker->printStats(std::cout);
103
151
        }
143
191
                  << LTL::to_string(options.ltlalgorithm)
144
192
                  << (result.is_weak ? " WEAK_SKIP" : "")
145
193
                  << ((options.stubbornreduction && !negated_formula->containsNext()) ? " STUBBORN" : "")
 
194
                  << (result.loopInvariantReduction ? " LOOP_INVARIANT_REDUCTION" : "")
146
195
                  << std::endl;
147
196
        /*(queries[qid]->isReachability(0) ? " REACHABILITY" : "") <<*/
148
197