Merge lp:~tapaal-ltl/verifypn/ltl-trace-fixes into lp:verifypn

[Nikolaj Jensen Ulrik]

Fix misunderstanding of trace formats for LTL traces.

[lp:~tapaal-ltl/verifypn/ltl-trace-fixes]

251. By Nikolaj Jensen Ulrik on 2021-08-06

Trace replay now works for non-LTL flows too

[Jiri Srba (srba)]

Only changes the trace behaviour, consistency check is not needed.

review: Approve

=== modified file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h	2021-08-03 14:19:42 +0000
+++ include/LTL/Algorithm/ModelChecker.h	2021-08-06 11:23:06 +0000
@@ -115,11 +115,22 @@
             if (traceLevel == TraceLevel::Full) {
                 os << ">";
                 os << std::endl;
-                for (size_t i = 0; i < net->numberOfPlaces(); ++i) {
+                auto [fpre, lpre] = net->preset(transition);
+                for(; fpre < lpre; ++fpre) {
+                    if (fpre->inhibitor) {
+                        assert(state.marking()[fpre->place] < fpre->tokens);
+                        continue;
+                    }
+                    for (size_t i = 0; i < fpre->tokens; ++i) {
+                        assert(state.marking()[fpre->place] >= fpre->tokens);
+                        os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[fpre->place] << "\"/>\n";
+                    }
+                }
+                /*for (size_t i = 0; i < net->numberOfPlaces(); ++i) {
                     for (size_t j = 0; j < state.marking()[i]; ++j) {
                         os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[i] << "\"/>\n";
                     }
-                }
+                }*/
                 os << indent << "</transition>";
             }
             else {

=== removed file 'include/LTL/Replay.h'
=== added file 'include/PetriEngine/TraceReplay.h'
--- include/PetriEngine/TraceReplay.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/TraceReplay.h	2021-08-06 11:23:06 +0000
@@ -0,0 +1,69 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_TRACEREPLAY_H
+#define VERIFYPN_TRACEREPLAY_H
+
+#include "PetriEngine/PetriNet.h"
+#include "PetriEngine/options.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "PetriEngine/SuccessorGenerator.h"
+
+#include <iostream>
+#include <utility>
+#include <rapidxml.hpp>
+
+namespace PetriEngine {
+    class TraceReplay {
+    public:
+        TraceReplay(std::istream &is, const PetriEngine::PetriNet *net, const options_t &options);
+
+        struct Token {
+            std::string place;
+        };
+
+        struct Transition {
+            explicit Transition(std::string id, int buchi) : id(std::move(id)), buchi_state(buchi) {}
+
+            std::string id;
+            int buchi_state;
+            std::unordered_map<uint32_t, uint32_t> tokens;
+        };
+
+        void parse(std::istream &xml, const PetriEngine::PetriNet *net);
+
+        bool replay(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond);
+
+        std::vector<Transition> trace;
+    private:
+
+        static constexpr auto DEADLOCK_TRANS = "##deadlock";
+        void parseRoot(const rapidxml::xml_node<> *pNode);
+
+        Transition parseTransition(const rapidxml::xml_node<char> *pNode);
+
+        void parseToken(const rapidxml::xml_node<char> *pNode, std::unordered_map<uint32_t, uint32_t> &current_marking);
+
+        size_t loop_idx = std::numeric_limits<size_t>::max();
+        std::unordered_map<std::string, int> transitions;
+        std::unordered_map<std::string, int> places;
+        bool _play_trace(const PetriEngine::PetriNet *net, PetriEngine::SuccessorGenerator &successorGenerator);
+        const options_t &options;
+    };
+}
+
+#endif //VERIFYPN_TRACEREPLAY_H

=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2021-07-22 09:46:13 +0000
+++ include/PetriEngine/options.h	2021-08-06 11:23:06 +0000
@@ -85,7 +85,7 @@
     BuchiOptimization buchiOptimization = BuchiOptimization::Low;
     const char* ltlHeuristic = "aut";
 
-    bool replay = false;
+    bool replay_trace = false;
     std::string replay_file;
 
 

=== modified file 'src/LTL/CMakeLists.txt'
--- src/LTL/CMakeLists.txt	2021-04-29 13:35:13 +0000
+++ src/LTL/CMakeLists.txt	2021-08-06 11:23:06 +0000
@@ -7,7 +7,7 @@
 add_subdirectory(Stubborn)
 add_subdirectory(SuccessorGeneration)
 
-add_library(LTL ${HEADER_FILES} LTLMain.cpp Replay.cpp)
+add_library(LTL ${HEADER_FILES} LTLMain.cpp)
 
 if (VERIFYPN_Static OR APPLE)
     target_link_libraries(LTL PRIVATE LTL_algorithm LTLStubborn LTL_simplification LTLSuccessorGeneration spot bddx)

=== removed file 'src/LTL/Replay.cpp'
=== modified file 'src/PetriEngine/CMakeLists.txt'
--- src/PetriEngine/CMakeLists.txt	2021-04-29 07:47:52 +0000
+++ src/PetriEngine/CMakeLists.txt	2021-08-06 11:23:06 +0000
@@ -15,6 +15,6 @@
 ReducingSuccessorGenerator.cpp
 STSolver.cpp
 SuccessorGenerator.cpp
-)
+        TraceReplay.cpp ../../include/PetriEngine/TraceReplay.h)
 
 target_link_libraries(PetriEngine PRIVATE Colored Structures Simplification Stubborn Reachability PQL TAR)

=== added file 'src/PetriEngine/TraceReplay.cpp'
--- src/PetriEngine/TraceReplay.cpp	1970-01-01 00:00:00 +0000
+++ src/PetriEngine/TraceReplay.cpp	2021-08-06 11:23:06 +0000
@@ -0,0 +1,237 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "PetriEngine/PQL/PQL.h"
+#include "PetriEngine/PetriNet.h"
+#include "PetriEngine/TraceReplay.h"
+#include "PetriEngine/Structures/State.h"
+#include "PetriEngine/SuccessorGenerator.h"
+#include "LTL/LTLToBuchi.h"
+
+#include <rapidxml.hpp>
+#include <vector>
+#include <iostream>
+#include <cstring>
+
+
+namespace PetriEngine {
+
+    TraceReplay::TraceReplay(std::istream &is, const PetriEngine::PetriNet *net, const options_t &options)
+        :options(options) {
+        parse(is, net);
+    }
+
+    void TraceReplay::parse(std::istream &xml, const PetriNet *net) {
+        places.clear();
+        transitions.clear();
+        // preallocate reverse lookup for transition and place names. Assume this is always called with the same Petri net.
+        for (int i = 0; i < net->placeNames().size(); ++i) {
+            places[net->placeNames()[i]] = i;
+        }
+        for (int i = 0; i < net->transitionNames().size(); ++i) {
+            transitions[net->transitionNames()[i]] = i;
+        }
+        transitions[DEADLOCK_TRANS] = -1;
+
+        // TODO can also validate transition names up front.
+        rapidxml::xml_document<> doc;
+        std::vector<char> buffer((std::istreambuf_iterator<char>(xml)), std::istreambuf_iterator<char>());
+        buffer.push_back('\0');
+        doc.parse<0>(buffer.data());
+        rapidxml::xml_node<> *root = doc.first_node();
+
+        if (root) {
+            parseRoot(root);
+        } else {
+            std::cerr << "Error getting root node." << std::endl;
+            assert(false);
+            exit(1);
+        }
+
+    }
+
+    void TraceReplay::parseRoot(const rapidxml::xml_node<> *pNode) {
+        if (std::strcmp(pNode->name(), "trace") != 0) {
+            std::cerr << "Error: Expected trace node. Got: " << pNode->name() << std::endl;
+            assert(false);
+            exit(1);
+        }
+        for (auto it = pNode->first_node(); it; it = it->next_sibling()) {
+            if (std::strcmp(it->name(), "loop") == 0) loop_idx = trace.size();
+            else if (std::strcmp(it->name(), "transition") == 0 || std::strcmp(it->name(), "deadlock") == 0) {
+                trace.push_back(parseTransition(it));
+            } else {
+                std::cerr << "Error: Expected transition or loop node. Got: " << it->name() << std::endl;
+                assert(false);
+                exit(1);
+            }
+        }
+        if (loop_idx == std::numeric_limits<size_t>::max() && options.logic == TemporalLogic::LTL) {
+            std::cerr << "Error: Missing <loop/> statement in trace\n";
+            exit(1);
+        }
+    }
+
+    TraceReplay::Transition TraceReplay::parseTransition(const rapidxml::xml_node<char> *pNode) {
+        std::string id;
+        int buchi = -1;
+        for (auto it = pNode->first_attribute(); it; it = it->next_attribute()) {
+            if (std::strcmp(it->name(), "id") == 0) {
+                id = std::string(it->value());
+            }
+            if (std::strstr(it->name(), "buchi") != nullptr) {
+                // buchi field is sometimes spelled slightly differently, but will always contain 'buchi'
+                buchi = std::stoi(it->value());
+            }
+        }
+        if (strcmp(pNode->name(), "deadlock") == 0) {
+            id = DEADLOCK_TRANS;
+        }
+        if (id.empty()) {
+            std::cerr << "Error: Transition has no id attribute" << std::endl;
+            assert(false);
+            exit(1);
+        }
+
+        Transition transition(id, buchi);
+
+        for (auto it = pNode->first_node(); it; it = it->next_sibling()) {
+            if (std::strcmp(it->name(), "token") != 0) {
+                std::cerr << "Warning: Unexpected transition child. Expected: token, but got: " << it->name()
+                          << std::endl;
+            }
+            parseToken(it, transition.tokens);
+        }
+
+        return transition;
+    }
+
+    void
+    TraceReplay::parseToken(const rapidxml::xml_node<char> *pNode,
+                            std::unordered_map<uint32_t, uint32_t> &current_marking) {
+        for (auto it = pNode->first_attribute(); it; it = it->next_attribute()) {
+            if (std::strcmp(it->name(), "place") == 0) {
+                std::string val{it->value()};
+                if (current_marking.find(places.at(val)) == current_marking.end()) {
+                    current_marking[places.at(val)] = 1;
+                } else {
+                    ++current_marking[places.at(val)];
+                }
+            }
+        }
+    }
+
+    bool TraceReplay::replay(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond) {
+        //spot::print_dot(std::cerr, buchiGenerator.aut._buchi);
+        PetriEngine::Structures::State state;
+        state.setMarking(net->makeInitialMarking());
+        PetriEngine::SuccessorGenerator successorGenerator(*net);
+
+        std::cout << "Playing back trace. Length: " << trace.size() << std::endl;
+        if (_play_trace(net, successorGenerator)) {
+            std::cout << "Replay complete. No errors" << std::endl;
+            return true;
+        }
+        return false;
+    }
+
+    bool
+    TraceReplay::_play_trace(const PetriEngine::PetriNet *net, PetriEngine::SuccessorGenerator &successorGenerator) {
+        PetriEngine::Structures::State state;
+        PetriEngine::Structures::State loopstate;
+        bool looping = false;
+        state.setMarking(net->makeInitialMarking());
+        loopstate.setMarking(net->makeInitialMarking());
+        for (int i = 0; i < trace.size(); ++i) {
+            const Transition &transition = trace[i];
+            // looping part should end up at the state _before_ the <loop/> tag,
+            // hence copy state from previous iteration.
+            if (i == loop_idx) {
+                memcpy(loopstate.marking(), state.marking(), sizeof(uint32_t) * net->numberOfPlaces());
+                looping = true;
+            }
+            successorGenerator.prepare(&state);
+            auto it = transitions.find(transition.id);
+            if (it == std::end(transitions)) {
+                std::cerr << "Unrecognized transition name " << transition.id << std::endl;
+                assert(false);
+                exit(1);
+            }
+            int tid = it->second;
+
+            if (tid != -1) {
+                // fire transition
+                if (!successorGenerator.checkPreset(tid)) {
+                    std::cerr
+                            << "ERROR the provided trace cannot be replayed on the provided model. \nOffending transition: "
+                            << transition.id << " at index: " << i << "\n";
+                    return false;
+                }
+                successorGenerator.consumePreset(state, tid);
+                successorGenerator.producePostset(state, tid);
+            } else {
+                // -1 is deadlock, assert deadlocked state.
+                // LTL deadlocks are unambiguously in the Petri net, since Büchi deadlocks won't generate any successor in the first place.
+                assert(i == trace.size() - 1);
+                if (!net->deadlocked(state.marking())) {
+                    std::cerr << "ERROR: Trace claimed the net was deadlocked, but there are enabled transitions.\n";
+                    return false;
+                }
+                return true;
+            }
+
+            if (!transition.tokens.empty()) {
+                auto[finv, linv] = net->preset(transitions.at(transition.id));
+                for (; finv != linv; ++finv) {
+                     if (finv->inhibitor) {
+
+                    } else {
+                        auto it = transition.tokens.find(finv->place);
+                        if (it == std::end(transition.tokens)) {
+                            std::cerr << "ERROR: Pre-place " << net->placeNames()[finv->place] << " of transition "
+                                      << transition.id << " was not mentioned in trace.\n";
+                            return false;
+                        }
+                        if (it->second != finv->tokens) {
+                            std::cerr << "ERROR: Pre-place " << net->placeNames()[finv->place] << " of transition "
+                                      << transition.id << "has arc weight " << finv->tokens << " but trace consumes "
+                                      << it->second << " tokens.\n";
+                            return false;
+                        }
+                    }
+                }
+            }
+        }
+
+        bool err = false;
+        if (looping) {
+            for (int i = 0; i < net->numberOfPlaces(); ++i) {
+                if (state.marking()[i] != loopstate.marking()[i]) {
+                    if (!err) {
+                        std::cerr << "ERROR end state not equal to expected loop state.\n";
+                        err = true;
+                    }
+                    std::cerr << "  " << net->placeNames()[i] << ": expected" << loopstate.marking()[i] << ", actual "
+                              << state.marking()[i] << '\n';
+                }
+            }
+        }
+
+        return !err;
+    }
+}
+

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-08-03 12:00:44 +0000
+++ src/VerifyPN.cpp	2021-08-06 11:23:06 +0000
@@ -86,7 +86,7 @@
 #include "PetriEngine/PQL/Expressions.h"
 #include "PetriEngine/Colored/ColoredPetriNetBuilder.h"
 #include "LTL/LTL.h"
-#include "LTL/Replay.h"
+#include "PetriEngine/TraceReplay.h"
 #include "LTL/LTLMain.h"
 
 #include <atomic>
@@ -393,8 +393,8 @@
             }
             ++i;
         }
-        else if (strcmp(argv[i], "--replay") == 0) {
-            options.replay = true;
+        else if (strcmp(argv[i], "--trace-replay") == 0) {
+            options.replay_trace = true;
             options.replay_file = std::string(argv[++i]);
         }
 
@@ -584,9 +584,12 @@
                     "                                       simplification and Büchi construction, but gives worse\n"
                     "                                       results since there is less opportunity for optimizations.\n"
                     "  --noverify                           Disable verification e.g. for getting unfolded net\n"
-                    "  --replay <file>                      Replays an LTL trace output by the --trace option.\n"
+                    "  --trace-replay <file>                Replays a trace as output by the --trace option.\n"
                     "                                       The trace is verified against the provided model and query.\n"
-                    "  --spot-optimization <1,2,3>          The optimization level passed to Spot for büchi creation. 1: Low (default), 2: Medium, 3: High\n"
+                    "                                       Mainly useful for debugging.\n"
+                    "  --spot-optimization <1,2,3>          The optimization level passed to Spot for Büchi automaton creation.\n"
+                    "                                       1: Low (default), 2: Medium, 3: High\n"
+                    "                                       Using optimization levels above 1 may cause exponential blowups and is not recommended.\n"
                     "\n"
                     "Return Values:\n"
                     "  0   Successful, query satisfiable\n"
@@ -625,17 +628,20 @@
             return SuccessCode;
         }
         else if (strcmp(argv[i], "--ltl-heur-help") == 0) {
-            printf("Heuristics for LTL model checking are specified using the following grammar:"
+            printf("Heuristics for LTL model checking are specified using the following grammar:\n"
                    "  heurexp : {'aut' | 'automaton'}\n"
                    "          | {'dist' | 'distance'}\n"
-                   "          | {'fc' | 'firecount' | 'fire-count'} INT\n"
+                   "          | {'fc' | 'firecount' | 'fire-count'} <threshold>?\n"
                    "          | '(' heurexp ')'\n"
                    "          | 'sum' <weight>? heurexp <weight?> heurexp\n"
                    "          | 'sum' '(' <weight>? heurexp ',' <weight>? heurexp ')'\n"
                    "Example strings:\n"
-                   "  - 'aut' - use the automaton heuristic for verification.\n"
+                   "  - aut - use the automaton heuristic for verification.\n"
                    "  - sum dist fc 1000 - use the sum of distance heuristic and fire count heuristic with threshold 1000.\n"
+                   "Weight for sum and threshold for fire count are optional and integral.\n"
+                   "Sum weights default to 1 (thus plain sum), and default fire count threshold is 5000.\n"
                    );
+            return SuccessCode;
         }
         else if (options.modelfile == NULL) {
             options.modelfile = argv[i];
@@ -725,8 +731,8 @@
         }
     }
 
-    if (options.replay && options.logic != TemporalLogic::LTL) {
-        std::cerr << "Argument Error: Trace replay is only supported for LTL model checking." << std::endl;
+    if (false && options.replay_trace && options.logic != TemporalLogic::LTL) {
+        std::cerr << "Argument Error: Trace replay_trace is only supported for LTL model checking." << std::endl;
         return ErrorCode;
     }
 
@@ -1493,24 +1499,23 @@
 
     if(alldone) return SuccessCode;
 
-    if (options.replay) {
+    if (options.replay_trace) {
         if (contextAnalysis(cpnBuilder, builder, net.get(), queries) != ContinueCode) {
             std::cerr << "Fatal error assigning indexes" << std::endl;
             exit(1);
         }
         std::ifstream replay_file(options.replay_file, std::ifstream::in);
-        LTL::Replay replay{replay_file, net.get()};
-        for (int i = 0; i < results.size(); ++i) {
-            if (results[i] == ResultPrinter::LTL) {
-                replay.replay(net.get(), queries[i], options);
-            }
+        PetriEngine::TraceReplay replay{replay_file, net.get(), options};
+        for (size_t i=0; i < queries.size(); ++i) {
+            if (results[i] == ResultPrinter::Unknown || results[i] == ResultPrinter::CTL || results[i] == ResultPrinter::LTL)
+                replay.replay(net.get(), queries[i]);
         }
         return SuccessCode;
     }
 
     if(options.doVerification){
 
-    //----------------------- Verify CTL queries -----------------------//
+        //----------------------- Verify CTL queries -----------------------//
         std::vector<size_t> ctl_ids;
         std::vector<size_t> ltl_ids;
         for(size_t i = 0; i < queries.size(); ++i)
@@ -1522,19 +1527,19 @@
             else if (results[i] == ResultPrinter::LTL) {
                 ltl_ids.push_back(i);
             }
-    }
+        }
 
-    if (options.replay) {
-        if (contextAnalysis(cpnBuilder, builder, net.get(), queries) != ContinueCode) {
-            std::cerr << "Fatal error assigning indexes" << std::endl;
-            exit(1);
-        }
-        std::ifstream replay_file(options.replay_file, std::ifstream::in);
-        LTL::Replay replay{replay_file, net.get()};
-        for (int i : ltl_ids) {
-            replay.replay(net.get(), queries[i], options);
-        }
-        return SuccessCode;
+        if (options.replay_trace) {
+            if (contextAnalysis(cpnBuilder, builder, net.get(), queries) != ContinueCode) {
+                std::cerr << "Fatal error assigning indexes" << std::endl;
+                exit(1);
+            }
+            std::ifstream replay_file(options.replay_file, std::ifstream::in);
+            PetriEngine::TraceReplay replay{replay_file, net.get(), options};
+            for (int i : ltl_ids) {
+                replay.replay(net.get(), queries[i]);
+            }
+            return SuccessCode;
         }
 
         if (!ctl_ids.empty()) {