=== modified file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h 2021-02-01 11:17:38 +0000
+++ include/LTL/Algorithm/ModelChecker.h 2021-03-04 10:04:52 +0000
@@ -21,24 +21,37 @@
#include "PetriEngine/PQL/PQL.h"
#include "LTL/ProductSuccessorGenerator.h"
#include "LTL/Algorithm/ProductPrinter.h"
+#include "PetriEngine/options.h"
namespace LTL {
+
class ModelChecker {
public:
- ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak);
+ ModelChecker(const PetriEngine::PetriNet &net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak,
+ TraceLevel level = TraceLevel::Transitions);
+
virtual bool isSatisfied() = 0;
-
+
virtual ~ModelChecker() = default;
+
[[nodiscard]] bool isweak() const { return is_weak; }
+
+
protected:
std::unique_ptr successorGenerator;
const PetriEngine::PetriNet &net;
PetriEngine::PQL::Condition_ptr formula;
+ TraceLevel traceLevel;
size_t _discovered = 0;
const bool shortcircuitweak;
bool weakskip = false;
bool is_weak = false;
+ int maxTransName;
+
+ std::ostream &printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os);
+
+ void printLoop(std::ostream &os);
};
}
=== modified file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-03-02 12:06:17 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-03-04 10:04:52 +0000
@@ -50,8 +50,8 @@
template
class NestedDepthFirstSearch : public ModelChecker {
public:
- NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak)
- : ModelChecker(net, ptr, shortcircuitweak), factory{net, successorGenerator->initial_buchi_state()},
+ NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak, TraceLevel level = TraceLevel::Full)
+ : ModelChecker(net, ptr, shortcircuitweak, level), factory{net, successorGenerator->initial_buchi_state()},
states(net, 0, (int)net.numberOfPlaces() + 1) {}
bool isSatisfied() override;
@@ -73,14 +73,13 @@
bool violation = false;
//Used for printing the trace
- std::stack nested_transitions;
+ std::stack> nested_transitions;
void dfs();
void ndfs(State &state);
- void printTrace(stack &transitions);
+ void printTrace(std::stack> &transitions, std::ostream &os = std::cout);
- ostream & printTransition(size_t transition, uint indent, ostream &os = std::cerr);
static constexpr bool SaveTrace = std::is_same_v;
};
extern template class NestedDepthFirstSearch;
=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h 2021-03-02 12:06:17 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h 2021-03-04 10:04:52 +0000
@@ -28,6 +28,7 @@
namespace LTL {
+<<<<<<< TREE
/**
* Implements on-the-fly version of Tarjan's algorithm suitable for LTL model checking.
* The idea is to detect some reachable strongly connected component containing an accepting state,
@@ -40,11 +41,27 @@
*
*/
template
+=======
+ /**
+ * Implements on-the-fly version of Tarjan's algorithm suitable for LTL model checking.
+ * The idea is to detect some reachable strongly connected component containing an accepting state,
+ * which constitutes a counter-example.
+ * For more details see
+ * Jaco Geldenhuys & Antti Valmari,
+ * More efficient on-the-fly LTL verification with Tarjan's algorithm,
+ * https://doi.org/10.1016/j.tcs.2005.07.004
+ *
+ * @tparam SaveTrace whether to save and print counter-examples when possible.
+ */
+ template
+>>>>>>> MERGE-SOURCE
class TarjanModelChecker : public ModelChecker {
public:
- TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond, const bool shortcircuitweak)
- : ModelChecker(net, cond, shortcircuitweak), factory(net, successorGenerator->initial_buchi_state()),
- seen(net, 0, (int) net.numberOfPlaces() + 1) {
+ TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond, const bool shortcircuitweak,
+ TraceLevel level = TraceLevel::Full)
+ : ModelChecker(net, cond, shortcircuitweak, level), factory(net, successorGenerator->initial_buchi_state()),
+ seen(net, 0, (int) net.numberOfPlaces() + 1)
+ {
chash.fill(std::numeric_limits::max());
}
@@ -58,7 +75,9 @@
LTL::Structures::ProductStateFactory factory;
- PetriEngine::Structures::StateSet seen;
+ using StateSet = std::conditional_t;
+
+ StateSet seen;
std::unordered_set store;
// rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack
@@ -66,7 +85,8 @@
std::array chash;
static_assert(sizeof(chash) == (1U << 27U));
- static inline idx_t hash(idx_t id) {
+ static inline idx_t hash(idx_t id)
+ {
return id % HashSz;
}
@@ -86,21 +106,27 @@
};
using CEntry = std::conditional_t;
+ TracableCEntry,
+ PlainCEntry>;
+
struct DEntry {
idx_t pos; // position in cstack.
successor_info sucinfo;
};
+<<<<<<< TREE
// master list of state information.
+=======
+>>>>>>> MERGE-SOURCE
std::vector cstack;
// depth-first search stack, contains current search path.
std::stack dstack;
// cstack positions of accepting states in current search path, for quick access.
std::stack astack;
bool violation = false;
+ size_t loopstate = std::numeric_limits::max();
+ size_t looptrans = std::numeric_limits::max();
void push(State &state);
@@ -108,12 +134,19 @@
void update(idx_t to);
- bool nexttrans(State &state, State& parent, DEntry &delem);
+ bool nexttrans(State &state, State &parent, DEntry &delem);
void popCStack();
+
+ void printTrace(std::stack &&dstack, std::ostream &os = std::cout);
+
};
-extern template class TarjanModelChecker;
-extern template class TarjanModelChecker;
+
+ extern template
+ class TarjanModelChecker;
+
+ extern template
+ class TarjanModelChecker;
}
#endif //VERIFYPN_TARJANMODELCHECKER_H
=== added file 'include/LTL/AlgorithmTypes.h'
--- include/LTL/AlgorithmTypes.h 1970-01-01 00:00:00 +0000
+++ include/LTL/AlgorithmTypes.h 2021-03-04 10:04:52 +0000
@@ -0,0 +1,41 @@
+/* Copyright (C) 2021 Nikolaj J. Ulrik ,
+ * Simon M. Virenfeldt
+ *
+ * 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 .
+ */
+
+#ifndef VERIFYPN_ALGORITHMTYPES_H
+#define VERIFYPN_ALGORITHMTYPES_H
+
+namespace LTL {
+ enum class Algorithm {
+ NDFS, RandomNDFS, Tarjan, None=-1
+ };
+ inline auto to_string(Algorithm alg) {
+ switch (alg) {
+ case Algorithm::NDFS:
+ return "NDFS";
+ case Algorithm::RandomNDFS:
+ return "RNDFS";
+ case Algorithm::Tarjan:
+ return "TARJAN";
+ case Algorithm::None:
+ default:
+ std::cerr << "to_string: Invalid LTL Algorithm " << static_cast(alg) << '\n';
+ assert(false);
+ }
+ }
+}
+
+#endif //VERIFYPN_ALGORITHMTYPES_H
=== modified file 'include/LTL/LTL.h'
--- include/LTL/LTL.h 2021-02-01 11:17:38 +0000
+++ include/LTL/LTL.h 2021-03-04 10:04:52 +0000
@@ -26,23 +26,7 @@
#include "LTL/LTLToBuchi.h"
namespace LTL {
- enum class Algorithm {
- NDFS, RandomNDFS, Tarjan, None=-1
- };
- inline auto to_string(Algorithm alg) {
- switch (alg) {
- case Algorithm::NDFS:
- return "NDFS";
- case Algorithm::RandomNDFS:
- return "RNDFS";
- case Algorithm::Tarjan:
- return "TARJAN";
- case Algorithm::None:
- default:
- std::cerr << "to_string: Invalid LTL Algorithm " << static_cast(alg) << '\n';
- assert(false);
- }
- }
+
std::pair to_ltl(const Condition_ptr &formula);
}
=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h 2021-01-08 09:12:40 +0000
+++ include/PetriEngine/options.h 2021-03-04 10:04:52 +0000
@@ -9,13 +9,19 @@
#include "Reachability/ReachabilitySearch.h"
#include "../CTL/Algorithm/AlgorithmTypes.h"
-#include "../LTL/LTL.h"
+#include "../LTL/AlgorithmTypes.h"
enum class TemporalLogic {
CTL, LTL
};
+enum class TraceLevel {
+ None,
+ Transitions,
+ Full
+};
+
struct options_t {
// bool outputtrace = false;
int kbound = 0;
@@ -29,7 +35,7 @@
bool printstatistics = true;
std::set querynumbers;
PetriEngine::Reachability::Strategy strategy = PetriEngine::Reachability::DEFAULT;
- bool trace = false;
+ TraceLevel trace = TraceLevel::None;
bool use_query_reductions = true;
int queryReductionTimeout = 30, lpsolveTimeout = 10;
uint32_t siphontrapTimeout = 0;
@@ -78,7 +84,7 @@
optionsOut = "\nSearch=OverApprox";
}
- if (trace) {
+ if (trace != TraceLevel::None) {
optionsOut += ",Trace=ENABLED";
} else {
optionsOut += ",Trace=DISABLED";
=== modified file 'src/CMakeLists.txt'
--- src/CMakeLists.txt 2021-02-01 11:17:38 +0000
+++ src/CMakeLists.txt 2021-03-04 10:04:52 +0000
@@ -5,7 +5,7 @@
add_subdirectory(PetriParse)
add_subdirectory(PetriEngine)
-add_executable(verifypn-${ARCH_TYPE} VerifyPN.cpp)
+add_executable(verifypn-${ARCH_TYPE} VerifyPN.cpp ../include/LTL/AlgorithmTypes.h)
add_dependencies(verifypn-${ARCH_TYPE} glpk-ext spot-ext)
target_link_libraries(verifypn-${ARCH_TYPE} PRIVATE CTL LTL PetriEngine PetriParse glpk spot)
=== modified file 'src/LTL/Algorithm/LTLToBuchi.cpp'
=== modified file 'src/LTL/Algorithm/ModelChecker.cpp'
--- src/LTL/Algorithm/ModelChecker.cpp 2021-02-01 11:17:38 +0000
+++ src/LTL/Algorithm/ModelChecker.cpp 2021-03-04 10:04:52 +0000
@@ -18,16 +18,54 @@
#include "LTL/Algorithm/ModelChecker.h"
#include
+#include
namespace LTL {
- ModelChecker::ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr condition, const bool shortcircuitweak)
- : net(net), formula(condition), shortcircuitweak(shortcircuitweak)
+ ModelChecker::ModelChecker(const PetriEngine::PetriNet &net, PetriEngine::PQL::Condition_ptr condition,
+ const bool shortcircuitweak, TraceLevel level)
+ : net(net), formula(condition), traceLevel(level), shortcircuitweak(shortcircuitweak)
{
successorGenerator = std::make_unique(net, condition);
- //TODO Create successor generator from net and condition
-
- //LTL::ProductPrinter::printProduct(*successorGenerator, std::cout, net, condition);
- }
+
+ maxTransName = std::max_element(std::begin(net.transitionNames()), std::end(net.transitionNames()),
+ [](auto &a, auto &b) { return a.size() < b.size(); })->size();
+
+ }
+
+ static constexpr auto indent = " ";
+ static constexpr auto tokenIndent = " ";
+
+ void ModelChecker::printLoop(std::ostream &os)
+ {
+ os << indent << "\n";
+ }
+
+ std::ostream &
+ ModelChecker::printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os)
+ {
+ if (transition >= std::numeric_limits::max() - 1) {
+ os << indent << "";
+ return os;
+ }
+ std::string tname = net.transitionNames()[transition];
+ if (traceLevel == TraceLevel::Full) {
+ os << indent << "\n";
+ for (size_t i = 0; i < net.numberOfPlaces(); ++i) {
+ for (size_t j = 0; j < state.marking()[i]; ++j) {
+ os << tokenIndent << R"(\n";
+ }
+ }
+#ifndef NDEBUG
+ os << '\n' << tokenIndent << "\n";
+#endif
+ os << indent << "";
+ } else {
+ os << indent << "";
+ }
+ return os;
+ }
+
}
=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-03-02 12:06:17 +0000
+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-03-04 10:04:52 +0000
@@ -19,14 +19,16 @@
namespace LTL {
template
- bool NestedDepthFirstSearch::isSatisfied() {
+ bool NestedDepthFirstSearch::isSatisfied()
+ {
is_weak = successorGenerator->is_weak() && shortcircuitweak;
dfs();
return !violation;
}
template
- void NestedDepthFirstSearch::dfs() {
+ void NestedDepthFirstSearch::dfs()
+ {
std::stack call_stack;
std::stack todo;
@@ -59,13 +61,13 @@
ndfs(curState);
if (violation) {
if constexpr (SaveTrace) {
- std::stack transitions;
+ std::stack> transitions;
size_t next = top.id;
states.decode(working, next);
while (!successorGenerator->isInitialState(working)) {
auto[parent, transition] = states.getHistory(next);
+ transitions.push(std::make_pair(next, transition));
next = parent;
- transitions.push(transition);
states.decode(working, next);
}
printTrace(transitions);
@@ -90,7 +92,8 @@
}
template
- void NestedDepthFirstSearch::ndfs(State &state) {
+ void NestedDepthFirstSearch::ndfs(State &state)
+ {
std::stack todo;
State working = factory.newState();
@@ -115,22 +118,22 @@
violation = true;
if constexpr (SaveTrace) {
auto[_, stateid] = states.add(working);
+ auto seedId = stateid;
states.setHistory2(stateid, successorGenerator->fired());
size_t next = stateid;
+<<<<<<< TREE
ptrie::uint trans = 0;
// SuccessorGenerator returns tcount - 1, but resets tcount to UINT_MAX when done,
// hence loop until transition >= UINT_MAX - 1.
while (trans < std::numeric_limits::max() - 1) {
+=======
+ // follow trace until back at seed state.
+ do {
+>>>>>>> MERGE-SOURCE
auto[state, transition] = states.getHistory2(next);
- if (transition >= std::numeric_limits::max() - 1) {
- auto[_, transition] = states.getHistory(next);
- nested_transitions.push(transition);
- break;
- }
+ nested_transitions.push(std::make_pair(next, transition));
next = state;
- trans = transition;
- nested_transitions.push(transition);
- }
+ } while (next != seedId);
}
return;
}
@@ -151,29 +154,26 @@
}
template
- ostream &NestedDepthFirstSearch::printTransition(size_t transition, uint indent, ostream &os) {
- if (transition == std::numeric_limits::max() - 1) {
- os << std::string(indent, '\t') << "";
- return os;
- }
- std::string tname = states.net().transitionNames()[transition];
- os << std::string(indent, '\t') << "";
- return os;
- }
-
- template
- void NestedDepthFirstSearch::printTrace(std::stack &transitions) {
- std::cerr << "Trace:\n\n";
+ void NestedDepthFirstSearch::printTrace(std::stack> &transitions, std::ostream &os)
+ {
+ State state = factory.newState();
+ os << "\n"
+ "\n";
while (!transitions.empty()) {
- printTransition(transitions.top(), 1) << std::endl;
+ auto [stateid, transition] = transitions.top();
+ states.decode(state, stateid);
+ printTransition(transition, state, os) << std::endl;
transitions.pop();
}
- std::cerr << "\t" << std::endl;
+ printLoop(os);
while (!nested_transitions.empty()) {
- printTransition(nested_transitions.top(), 2) << std::endl;
+ auto [stateid, transition] = nested_transitions.top();
+ states.decode(state, stateid);
+
+ printTransition(transition, state, os) << std::endl;
nested_transitions.pop();
}
- std::cerr << "\t" << std::endl << "" << std::endl;
+ os << std::endl << "" << std::endl;
}
=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
--- src/LTL/Algorithm/TarjanModelChecker.cpp 2021-03-02 12:06:17 +0000
+++ src/LTL/Algorithm/TarjanModelChecker.cpp 2021-03-04 10:04:52 +0000
@@ -47,7 +47,12 @@
pop();
continue;
}
- const idx_t stateid = seen.add(working).second;
+ auto[isnew, stateid] = seen.add(working);
+ if constexpr (SaveTrace) {
+ if (isnew) {
+ seen.setHistory(stateid, successorGenerator->fired());
+ }
+ }
dtop.sucinfo.last_state = stateid;
// lookup successor in 'hash' table
@@ -68,46 +73,13 @@
if constexpr (SaveTrace) {
// print counter-example if it exists.
if (violation) {
- State next = factory.newState();
- std::cerr << "Printing trace: " << std::endl;
- std::vector rev;
- auto sz = dstack.size();
- // dump stack to vector to allow iteration
- for (idx_t i = 0; i < sz; ++i) {
- rev.push_back(dstack.top());
+ std::stack revstack;
+ while (!dstack.empty()) {
+ revstack.push(std::move(dstack.top()));
dstack.pop();
}
- idx_t pos = 0;
- // print dstack in-order. rev[0] is dstack.top(), so loop vector in reverse
- for (int i = rev.size() - 1; i >= 0; --i) {
- pos = rev[i].pos;
- seen.decode(parent, cstack[pos].stateid);
- _dump_state(parent);
- cstack[pos].lowlink = std::numeric_limits::max();
- if (i > 0) {
- // print transition to next state
- seen.decode(next, cstack[rev[i - 1].pos].stateid);
- successorGenerator->prepare(&parent);
- while (successorGenerator->next(working)) {
- if (working == next) {
- std::cerr << net.transitionNames()[successorGenerator->last_transition()]
- << std::endl;
- break;
- }
- }
- }
- }
-
- // follow lowsource until back in dstack
- pos = cstack[pos].lowsource;
- if (cstack[pos].lowlink != std::numeric_limits::max()) {
- std::cerr << "Printing looping part\n";
- }
- while (cstack[pos].lowlink != std::numeric_limits::max()) {
- seen.decode(parent, cstack[pos].stateid);
- _dump_state(parent);
- pos = cstack[pos].lowsource;
- }
+ printTrace(std::move(revstack));
+ return false;
}
}
}
@@ -176,7 +148,10 @@
// either way update the component ID of the state we came from.
cstack[from].lowlink = cstack[to].lowlink;
if constexpr (SaveTrace) {
- cstack[from].lowsource = to;
+ loopstate = cstack[to].stateid;
+ looptrans = successorGenerator->fired();
+ cstack[from].lowsource = cstack[to].lowlink;
+
}
}
}
@@ -192,9 +167,46 @@
return res;
}
+
+ template
+ void TarjanModelChecker::printTrace(std::stack &&dstack, std::ostream &os)
+ {
+ if constexpr (!SaveTrace) {
+ return;
+ } else {
+ State state = factory.newState();
+ dstack.pop();
+ os << "\n"
+ "\n";
+ unsigned long p;
+ // print (reverted) dstack
+ while (!dstack.empty()) {
+ p = dstack.top().pos;
+ auto stateid = cstack[p].stateid;
+ auto[parent, tid] = seen.getHistory(stateid);
+ seen.decode(state, stateid);
+ printTransition(tid, state, os) << '\n';
+ cstack[p].lowlink = std::numeric_limits::max();
+ dstack.pop();
+ }
+ printLoop(os);
+ // follow previously found back edges via lowsource until back in dstack.
+ p = cstack[p].lowsource;
+ while (cstack[p].lowlink != std::numeric_limits::max()) {
+ auto[parent, tid] = seen.getHistory(cstack[p].stateid);
+ seen.decode(state, cstack[p].stateid);
+ printTransition(tid, state, os) << '\n';
+ p = cstack[p].lowsource;
+ }
+ printTransition(looptrans, state, os) << '\n';
+
+ os << "" << std::endl;
+ }
+ }
+
template
class TarjanModelChecker;
template
class TarjanModelChecker;
-}
\ No newline at end of file
+}
=== modified file 'src/PetriEngine/Reachability/ResultPrinter.cpp'
--- src/PetriEngine/Reachability/ResultPrinter.cpp 2020-04-23 15:26:52 +0000
+++ src/PetriEngine/Reachability/ResultPrinter.cpp 2021-03-04 10:04:52 +0000
@@ -132,7 +132,7 @@
if(options->cpnOverApprox)
std::cout << "\nSolved using CPN Approximation\n" << std::endl;
- if(showTrace && options->trace)
+ if(showTrace && options->trace != TraceLevel::None)
{
if(stateset == nullptr)
{
=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp 2021-03-03 08:34:27 +0000
+++ src/VerifyPN.cpp 2021-03-04 10:04:52 +0000
@@ -169,7 +169,22 @@
} else if (strcmp(argv[i], "-n") == 0 || strcmp(argv[i], "--no-statistics") == 0) {
options.printstatistics = false;
} else if (strcmp(argv[i], "-t") == 0 || strcmp(argv[i], "--trace") == 0) {
- options.trace = true;
+ if (argc > i + 1) {
+ if (strcmp("1", argv[i+1]) == 0) {
+ options.trace = TraceLevel::Transitions;
+ }
+ else if (strcmp("2", argv[i+1]) == 0) {
+ options.trace = TraceLevel::Full;
+ }
+ else {
+ options.trace = TraceLevel::Full;
+ continue;
+ }
+ ++i;
+ }
+ else {
+ options.trace = TraceLevel::Full;
+ }
} else if (strcmp(argv[i], "-x") == 0 || strcmp(argv[i], "--xml-queries") == 0) {
if (i == argc - 1) {
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
@@ -1122,7 +1137,7 @@
if (options.enablereduction > 0) {
// Compute how many times each place appears in the query
builder.startTimer();
- builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout, options.reductions);
+ builder.reduce(queries, results, options.enablereduction, options.trace != TraceLevel::None, nullptr, options.reductionTimeout, options.reductions);
printer.setReducer(builder.getReducer());
}
@@ -1199,9 +1214,9 @@
std::unique_ptr modelChecker;
switch (options.ltlalgorithm) {
case LTL::Algorithm::NDFS:
- if (options.trace)
+ if (options.trace != TraceLevel::None)
modelChecker = std::make_unique>
- (*net, negated_formula, options.ltluseweak);
+ (*net, negated_formula, options.ltluseweak, options.trace);
else
modelChecker = std::make_unique>
(*net, negated_formula, options.ltluseweak);
@@ -1209,8 +1224,8 @@
case LTL::Algorithm::RandomNDFS:
modelChecker = std::make_unique(*net, negated_formula);
case LTL::Algorithm::Tarjan:
- if (options.trace)
- modelChecker = std::make_unique>(*net, negated_formula, options.ltluseweak);
+ if (options.trace != TraceLevel::None)
+ modelChecker = std::make_unique>(*net, negated_formula, options.ltluseweak, options.trace);
else
modelChecker = std::make_unique>(*net, negated_formula, options.ltluseweak);
break;
@@ -1266,7 +1281,7 @@
//Reachability search
strategy.reachable(queries, results,
options.printstatistics,
- options.trace);
+ options.trace != TraceLevel::None);
}
else
{
@@ -1281,7 +1296,7 @@
options.stubbornreduction,
options.statespaceexploration,
options.printstatistics,
- options.trace);
+ options.trace != TraceLevel::None);
}
return SuccessCode;