From 7514797581b423c08dcf6d0a38e7e6fc6feb2822 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:37:46 +0200 Subject: [PATCH 01/16] Add -! cli option for immediate trace logging --- src/cli/CLIConfig.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/cli/CLIConfig.cpp b/src/cli/CLIConfig.cpp index c40caf56..0b1dbdc4 100644 --- a/src/cli/CLIConfig.cpp +++ b/src/cli/CLIConfig.cpp @@ -27,6 +27,9 @@ CLIConfig::CLIConfig() { { option_requirement::Optional, {"output", 'o', argument_requirement::REQUIRE_ARG, "[DIR]/[FILENAME] Output file. Will be created, if not already exists"} }, + { option_requirement::Optional, + {"immediate-output", '!', argument_requirement::NO_ARG, + "Immediately output a trace once a query has been satisfied"} }, { option_requirement::Optional, {"query", 'q', argument_requirement::REQUIRE_ARG, "[DIR]/[FILENAME] File with queries to be verified. This flag is required for verification"} }, From 5ed48c883e95f255b236c569b41c1eb83133fe6b Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:38:31 +0200 Subject: [PATCH 02/16] Print results immediately if -! flag is provided --- src/verifier/ReachabilitySearcher.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index fd1b313e..b37241e6 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -74,7 +74,7 @@ bool ReachabilitySearcher::IsQuerySatisfied(const Query& query, const TTA &state } void ReachabilitySearcher::AreQueriesSatisfied(std::vector& queries, const TTA& state, size_t state_hash) { - for(auto & query : queries) { + for(auto& query : queries) { if(!query.answer) { query.answer = IsQuerySatisfied(*query.query, state); if (query.answer) { @@ -83,6 +83,8 @@ void ReachabilitySearcher::AreQueriesSatisfied(std::vector& que auto ss = ConvertASTToString(*query.query); spdlog::info("Query '{0}' is satisfied!", ss); spdlog::debug("Query '{0}' was satisfied in state: \n{1}", ss, state.GetCurrentStateString()); + if(CLIConfig::getInstance()["immediate-output"]) + PrintResults({query}); } } } @@ -209,7 +211,7 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate while(stateit != Waiting.end()) { auto& state = stateit->second; auto curstatehash = stateit->first; - AreQueriesSatisfied(query_results, state.tta, curstatehash); + if(AreQueriesAnswered(query_results)) { Passed.emplace(std::make_pair(curstatehash, state)); if(CLIConfig::getInstance()["verbosity"] && CLIConfig::getInstance()["verbosity"].as_integer() >= 6) @@ -229,6 +231,7 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate AddToWaitingList(state.tta, allTickStateChanges, false, curstatehash); Passed.emplace(std::make_pair(curstatehash, state)); + AreQueriesSatisfied(query_results, state.tta, curstatehash); cleanup_waiting_list(*this, curstatehash, state); stateit = PickStateFromWaitingList(strategy); From d8738a529d89660ff6050448cb655f5a6c009dc3 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:40:10 +0200 Subject: [PATCH 03/16] Added operator== (and !=) for TTAs, and fixed a crucial bug in interestingness set generation --- src/runtime/TTA.cpp | 30 +++++++++++++++++++++++--- src/runtime/TTA.h | 3 +++ src/verifier/TTASuccessorGenerator.cpp | 4 ++-- 3 files changed, 32 insertions(+), 5 deletions(-) diff --git a/src/runtime/TTA.cpp b/src/runtime/TTA.cpp index 92cac694..bc3df8a0 100644 --- a/src/runtime/TTA.cpp +++ b/src/runtime/TTA.cpp @@ -22,11 +22,35 @@ #include #include +auto TTA::operator==(const TTA &other) -> bool { + for(auto& c : components) { + if(c.second.currentLocation.identifier != other.components.at(c.first).currentLocation.identifier) + return false; + } + for(auto& s : symbols.map()) { + if(s.second != other.symbols.map()[s.first]) + return false; + } + return true; +} + +auto TTA::operator!=(const TTA &other) -> bool { + return !(*this == other); +} + TTA::StateChange operator+(TTA::StateChange a, TTA::StateChange b) { // Merge a and b - a.symbols.map().merge(b.symbols.map()); - a.componentLocations.merge(b.componentLocations); - return a; + // a.symbols.map().merge(b.symbols.map()); + TTA::StateChange cpy{}; + for(auto& s : a.symbols.map()) + cpy.symbols[s.first] = s.second; + for(auto& s : b.symbols.map()) + cpy.symbols[s.first] = s.second; + for(auto& c : a.componentLocations) + cpy.componentLocations[c.first] = c.second; + for(auto& c : b.componentLocations) + cpy.componentLocations[c.first] = c.second; + return cpy; } TTA operator<<(const TTA& aa, const TTA::StateChange& b) { diff --git a/src/runtime/TTA.h b/src/runtime/TTA.h index f93a09ad..5092b8b8 100644 --- a/src/runtime/TTA.h +++ b/src/runtime/TTA.h @@ -127,6 +127,9 @@ struct TTA { TokenMap GetSymbolChangesAsMap(std::vector &symbolChanges) const; void WarnAboutComponentOverlap(component_overlap_t& overlappingComponents) const; bool TypeCheck(const std::pair &symbol, const std::map::iterator &changingSymbol) const; + /// WARNING: Very expensive operation! + auto operator==(const TTA& other) -> bool; + auto operator!=(const TTA& other) -> bool; }; struct StateMultiChoice { diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index 90ef76f8..2bace607 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -134,7 +134,7 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons while(!frontier.empty()) { auto statechange = frontier.top(); frontier.pop(); - auto& curr = statechange.first; + auto curr = statechange.first; auto& idx = statechange.second; if(idx >= a.size()) { crossProduct.push_back(statechange.first); @@ -142,7 +142,7 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons TTA::StateChange stA{}; AssignVariable(stA.symbols, derivedSymbols, a[idx].first, a[idx].second); TTA::StateChange stB{}; - AssignVariable(stB.symbols, derivedSymbols, a[idx].first, a[idx].second); + AssignVariable(stB.symbols, derivedSymbols, b[idx].first, b[idx].second); frontier.push(std::make_pair(curr + stA, idx+1)); frontier.push(std::make_pair(curr + stB, idx+1)); } From 138e08e3f12faf6513b3c4e45dd50683ec06e4b6 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:40:55 +0200 Subject: [PATCH 04/16] Only complain about hash collissions if they are actual state collissions I might revert this again someday --- src/verifier/ReachabilitySearcher.cpp | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index b37241e6..039c555f 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -119,8 +119,21 @@ auto ReachabilitySearcher::PrintResults(const std::vector& resu if(exists) { auto range = Passed.equal_range(stateHash); auto count = Passed.count(stateHash); - if(count > 1) - spdlog::warn("HASH COLLISIONS: {0}", count); + if(count > 1) { + std::stringstream ss{}; + int c = 0; + for (auto it = range.first; it != range.second; ++it) { + ss << it->second.tta.GetCurrentStateString(); + for(auto t = range.first; t != range.second; ++t) { + if(it->second.tta != t->second.tta) + c++; + } + } + if(c > 0) { + spdlog::warn("HASH COLLISIONS: {0}", c); + spdlog::warn(ss.str()); + } + } if(stateHash == range.first->second.prevStateHash) { spdlog::critical("Breaking out of infinite loop. Something is wrong."); @@ -129,10 +142,6 @@ auto ReachabilitySearcher::PrintResults(const std::vector& resu stateHash = range.first->second.prevStateHash; trace.push_back(range.first->second.tta.GetCurrentStateString()); - if(count > 1) { - for (auto it = range.first; it != range.second; ++it) - spdlog::warn(it->second.tta.GetCurrentStateString()); - } } else { spdlog::critical("Unable to resolve witnessing trace. "); break; From 0a552c6432c149c3792d1f0cf6e72948cbde8a94 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:41:31 +0200 Subject: [PATCH 05/16] Actually check for duplicate states when detecting already visited states --- src/verifier/ReachabilitySearcher.cpp | 28 +++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index 039c555f..736b29f6 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -271,12 +271,22 @@ void ReachabilitySearcher::AddToWaitingList(const TTA &state, const std::vector< /// This is a lot of copying large data objects... Figure something out with maybe std::move auto nstate = state << change; auto nstatehash = nstate.GetCurrentStateHash(); - if (Passed.find(nstatehash) == Passed.end()) { + auto passed_it = Passed.find(nstatehash); + if (passed_it == Passed.end()) { if (nstatehash == state_hash) { + if(nstate == state) + continue; spdlog::warn("Recursive state hashes!"); - continue; } Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked})); + } else { + auto r = Passed.equal_range(nstatehash); + for(auto it = r.first; it != r.second; ++it) { + if(nstate != it->second.tta) { + Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked})); + break; + } + } } } } @@ -289,12 +299,22 @@ void ReachabilitySearcher::AddToWaitingList(const TTA &state, const std::vector< /// This is a lot of copying large data objects... Figure something out with maybe std::move auto nstate = baseChanges << *it; auto nstatehash = nstate.GetCurrentStateHash(); - if (Passed.find(nstatehash) == Passed.end()) { + auto passed_it = Passed.find(nstatehash); + if (passed_it == Passed.end()) { if (nstatehash == state_hash) { + if(nstate == state) + continue; spdlog::warn("Recursive state hashes!"); - continue; } Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked})); + } else { + auto r = Passed.equal_range(nstatehash); + for(auto it = r.first; it != r.second; ++it) { + if(nstate != it->second.tta) { + Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked})); + break; + } + } } } } From bf8e3f68ebe07c2d6cc99a519f960223009e7d24 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:42:01 +0200 Subject: [PATCH 06/16] Fixed a bug with osx's filesystem thingy --- src/model_parsers/TTAParser.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/model_parsers/TTAParser.cpp b/src/model_parsers/TTAParser.cpp index e1a0acbc..02b920cd 100644 --- a/src/model_parsers/TTAParser.cpp +++ b/src/model_parsers/TTAParser.cpp @@ -28,6 +28,7 @@ std::vector componentIgnoreList = { // NOLINT(cert-err58-cpp) "ignore", // ignore all files that want to be ignored "Queries.json", // Queries are not component- or symbol-files ".parts", // parts files are not components + ".DS_Store", // OSX makes these files all the time. }; bool ShouldSkipEntry(const std::filesystem::directory_entry& entry) { From f9c0be2a69be0b2ae92ffba2c4776e76a0f9bd8d Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:42:12 +0200 Subject: [PATCH 07/16] Print Timers as doubles --- src/runtime/TTA.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/runtime/TTA.cpp b/src/runtime/TTA.cpp index bc3df8a0..5cf6d675 100644 --- a/src/runtime/TTA.cpp +++ b/src/runtime/TTA.cpp @@ -329,8 +329,12 @@ std::string TTA::GetCurrentStateString() const { std::stringstream ss{}; ss << "{"; for(auto& component : components) ss<<"\""<type == TIMER) + ss << "\"" << symbol.first << "\"" << ": " << "\"" << symbol.second.asDouble() << "\","; + else + ss << "\"" << symbol.first << "\"" << ": " << "\"" << symbol.second.str() << "\","; + } ss << R"("OBJECT_END":"true"})"; // This is just a bad way of ending a json object. return ss.str(); } From 49f58be95197d279bf8caf206a165960dc71859f Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:42:30 +0200 Subject: [PATCH 08/16] Hacked in C++11 randomness I still need a better seed --- src/verifier/ReachabilitySearcher.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index 736b29f6..736ed751 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -327,7 +327,8 @@ bool ReachabilitySearcher::AreQueriesAnswered(const std::vector bool ReachabilitySearcher::IsSearchStateTockable(const SearchState& state) { return (!state.justTocked && !state.tta.IsCurrentStateImmediate()); } - +#include +std::random_device r; ReachabilitySearcher::StateList::iterator ReachabilitySearcher::PickStateFromWaitingList(const nondeterminism_strategy_t& strategy) { if(Waiting.empty()) return Waiting.end(); @@ -341,14 +342,17 @@ ReachabilitySearcher::StateList::iterator ReachabilitySearcher::PickStateFromWai return Waiting.begin(); case nondeterminism_strategy_t::PICK_LAST: { auto begin = Waiting.begin(); - for (auto i = 0; i < Waiting.size(); i++) + for (auto i = 0; i < Waiting.size()-1; i++) begin++; return begin; } case nondeterminism_strategy_t::PICK_RANDOM: - auto randomPick = rand() % Waiting.size(); + // auto randomPick = rand() % Waiting.size(); + std::default_random_engine e1(r()); + std::uniform_int_distribution uniform_dist(0, Waiting.size()-1); + auto randomPick = uniform_dist(e1); auto picked = Waiting.begin(); - for(int i = 0; i < randomPick; i++) + for(auto i = 0; i < randomPick; i++) picked++; return picked; } From 23344e22c4cfa941acf57ed5ad487ab56629dda6 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Wed, 20 Apr 2022 16:43:41 +0200 Subject: [PATCH 09/16] v1.10.0 --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index e20ff954..8f18c65a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -16,7 +16,7 @@ # 3.16+ because of target_precompiled_header cmake_minimum_required(VERSION 3.16) -project(aaltitoad VERSION 0.9.2) +project(aaltitoad VERSION 0.10.0) configure_file(src/config.h.in config.h) set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED) From d2db357cc20fd0da0bcf9bb1cf80f10663ad5077 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 08:55:31 +0200 Subject: [PATCH 10/16] Add --print-memory cli option --- src/cli/CLIConfig.cpp | 3 +++ src/verifier/ReachabilitySearcher.cpp | 33 +++++++++++++++++---------- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/src/cli/CLIConfig.cpp b/src/cli/CLIConfig.cpp index 0b1dbdc4..8d1d97ec 100644 --- a/src/cli/CLIConfig.cpp +++ b/src/cli/CLIConfig.cpp @@ -63,6 +63,9 @@ CLIConfig::CLIConfig() { { option_requirement::Optional, {"notrace", 'c', argument_requirement::NO_ARG, "Disable print of traces to stdout"} }, + { option_requirement::Optional, + {"print-memory", 'g', argument_requirement::REQUIRE_ARG, + "[INTEGER] Periodically print (debug level) current searchspace size"} }, }; status_code = EXIT_SUCCESS; } diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index 736ed751..9f4cc6cd 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -75,18 +75,18 @@ bool ReachabilitySearcher::IsQuerySatisfied(const Query& query, const TTA &state void ReachabilitySearcher::AreQueriesSatisfied(std::vector& queries, const TTA& state, size_t state_hash) { for(auto& query : queries) { - if(!query.answer) { - query.answer = IsQuerySatisfied(*query.query, state); - if (query.answer) { - query.acceptingStateHash = state_hash; - query.acceptingState.tta = state; // TODO: This is terrible - auto ss = ConvertASTToString(*query.query); - spdlog::info("Query '{0}' is satisfied!", ss); - spdlog::debug("Query '{0}' was satisfied in state: \n{1}", ss, state.GetCurrentStateString()); - if(CLIConfig::getInstance()["immediate-output"]) - PrintResults({query}); - } - } + if(query.answer) + continue; + if(!IsQuerySatisfied(*query.query, state)) + continue; + query.answer = true; + query.acceptingStateHash = state_hash; + query.acceptingState.tta = state; // TODO: This is terrible + auto ss = ConvertASTToString(*query.query); + spdlog::info("Query '{0}' is satisfied!", ss); + spdlog::debug("Query '{0}' was satisfied in state: \n{1}", ss, state.GetCurrentStateString()); + if(CLIConfig::getInstance()["immediate-output"]) + PrintResults({query}); } } @@ -217,7 +217,16 @@ std::string debug_get_symbol_map_string_representation(const TTA::SymbolMap& map bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strategy_t& strategy) { auto stateit = Waiting.begin(); + Timer periodic_timer{}; + periodic_timer.start(); while(stateit != Waiting.end()) { + if(CLIConfig::getInstance()["print-memory"]) { + if(periodic_timer.milliseconds_elapsed() >= CLIConfig::getInstance()["print-memory"].as_integer()) { + spdlog::debug("Waiting list size: {0}", Waiting.size()); + periodic_timer.start(); + } + } + auto& state = stateit->second; auto curstatehash = stateit->first; From 04982f851d817d6bb53c0bc5fe5af144e789a917 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 09:06:14 +0200 Subject: [PATCH 11/16] Get the reference instead --- src/verifier/TTASuccessorGenerator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index 2bace607..e0b6dd55 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -134,7 +134,7 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons while(!frontier.empty()) { auto statechange = frontier.top(); frontier.pop(); - auto curr = statechange.first; + auto& curr = statechange.first; auto& idx = statechange.second; if(idx >= a.size()) { crossProduct.push_back(statechange.first); From de77af6dcf29768a500d56f80175b8a8717410ff Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 09:43:58 +0200 Subject: [PATCH 12/16] Fix a problem where b.size() could be less than a.size() --- src/runtime/TTA.cpp | 32 ++++++++++++-------------- src/verifier/TTASuccessorGenerator.cpp | 3 ++- 2 files changed, 17 insertions(+), 18 deletions(-) diff --git a/src/runtime/TTA.cpp b/src/runtime/TTA.cpp index 5cf6d675..9a42d120 100644 --- a/src/runtime/TTA.cpp +++ b/src/runtime/TTA.cpp @@ -192,33 +192,31 @@ bool TTA::SetComponentLocations(const ComponentLocationMap &locationChange) { bool TTA::SetSymbols(const SymbolMap &symbolChange) { for(auto& symbol : symbolChange.map()) { auto symbolit = symbols.map().find(symbol.first); - bool noerror = TypeCheck(symbol, symbolit); - if(noerror) { - symbols.map()[symbol.first] = symbol.second; - if(externalSymbols.find(symbol.first) != externalSymbols.end()) - externalSymbols[symbol.first] = symbols.find(symbol.first); - } - else return false; + if(!TypeCheck(symbol, symbolit)) + return false; + symbols.map()[symbol.first] = symbol.second; + if(externalSymbols.find(symbol.first) != externalSymbols.end()) + externalSymbols[symbol.first] = symbols.find(symbol.first); } return true; } bool TTA::TypeCheck(const std::pair &symbol, const std::map::iterator &changingSymbol) const { - auto x = symbol.second->type; - auto y = changingSymbol->second->type; if(changingSymbol == symbols.map().end()) { spdlog::critical("Attempted to change the state of TTA failed. Symbol '{0}' does not exist.", symbol.first); return false; - } else if(!(NUM & x & y) && !(x == VAR && (NUM & y))) { - auto a = tokenTypeToString(changingSymbol->second->type); - auto b = tokenTypeToString(symbol.second->type); - spdlog::critical( - "Attempted to change the state of TTA failed. Symbol '{0}' does not have the correct type. ({1} vs {2} (a := b))", - symbol.first, a, b); - return false; } - return true; + auto x = symbol.second->type; + auto y = changingSymbol->second->type; + if((NUM & x & y) || (x == VAR && (NUM & y)) || (x == y)) + return true; + auto a = tokenTypeToString(changingSymbol->second->type); + auto b = tokenTypeToString(symbol.second->type); + spdlog::critical( + "Attempted to change the state of TTA failed. Symbol '{0}' does not have the correct type. ({1} vs {2} (a := b))", + symbol.first, a, b); + return false; } bool TTA::IsCurrentStateImmediate() const { diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index e0b6dd55..3d61a710 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -123,6 +123,7 @@ void AssignVariable(TTA::SymbolMap& outputMap, const TTA::SymbolMap& currentValu [&](const std::string& v) { outputMap.map()[varname] = v; } ), newValue); } + /// This absolutely explodes into a billion pieces if the sizeof(a) or b becomes too large. /// i.e. just 16 changes equals 65536 stateChanges (2^N) /// - which is not something that doesnt happen @@ -136,7 +137,7 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons frontier.pop(); auto& curr = statechange.first; auto& idx = statechange.second; - if(idx >= a.size()) { + if(idx >= a.size() || idx >= b.size()) { crossProduct.push_back(statechange.first); } else { TTA::StateChange stA{}; From f60af6e40a42d5ed7b874dbd87a950683a165f9e Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 16:42:10 +0200 Subject: [PATCH 13/16] wip --- src/verifier/TTASuccessorGenerator.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index 3d61a710..acdf4def 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -124,6 +124,15 @@ void AssignVariable(TTA::SymbolMap& outputMap, const TTA::SymbolMap& currentValu ), newValue); } +std::vector SymbolsCrossProduct(const VariableValueVector& a, const VariableValueVector& b, const TTA::SymbolMap& derivedSymbols) { + std::unordered_multimap m{}; + for(auto& x : a) + m.emplace(x.first, x.second); + for(auto& y : b) + m.emplace(y.first, y.second); + // sizeof(keys) * for each key +} + /// This absolutely explodes into a billion pieces if the sizeof(a) or b becomes too large. /// i.e. just 16 changes equals 65536 stateChanges (2^N) /// - which is not something that doesnt happen From 98929da2b18ea13afb8416a90bb64123471a8546 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 20:35:46 +0200 Subject: [PATCH 14/16] Implemented crossproduct using bitvector hack (easier to understand, and actually correctly implemented) --- src/verifier/TTASuccessorGenerator.cpp | 78 +++++++++++++++++--------- 1 file changed, 50 insertions(+), 28 deletions(-) diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index acdf4def..189ed22d 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -100,8 +100,14 @@ bool TTASuccessorGenerator::IsStateInteresting(const TTA& ttaState) { [](const auto& edge){ return edge.ContainsExternalChecks(); }); } +struct SymbolNamePair { + SymbolNamePair(const std::string& varname, const TTASymbol_t& symbol) + : varname(varname), symbol(symbol) {} + std::string varname; + TTASymbol_t symbol; +}; using VariableValueCollection = std::set>; -using VariableValueVector = std::vector>; +using VariableValueVector = std::vector; void AssignVariable(TTA::SymbolMap& outputMap, const TTA::SymbolMap& currentValues, const std::string &varname, const TTASymbol_t &newValue) { std::visit(overload( @@ -124,13 +130,36 @@ void AssignVariable(TTA::SymbolMap& outputMap, const TTA::SymbolMap& currentValu ), newValue); } -std::vector SymbolsCrossProduct(const VariableValueVector& a, const VariableValueVector& b, const TTA::SymbolMap& derivedSymbols) { - std::unordered_multimap m{}; - for(auto& x : a) - m.emplace(x.first, x.second); - for(auto& y : b) - m.emplace(y.first, y.second); - // sizeof(keys) * for each key +void add(std::vector& v) { + for(auto i = 0; i < v.size(); i++) { + if(v[i]) + continue; + for(; i >= 0; i--) + v[i].flip(); + break; + } +} + +std::vector SymbolsCrossProduct(const VariableValueVector& positives, + const VariableValueVector& negatives, + unsigned int predicate_count, + const TTA::SymbolMap& derivedSymbols) { + std::vector return_value{}; + std::vector bitset(predicate_count); + for(auto i = 0; i < pow(2, predicate_count); i++) { + TTA::StateChange change{}; + auto j = 0; + for(auto b : bitset) { + if(b) + AssignVariable(change.symbols, derivedSymbols, positives[j].varname, positives[j].symbol); + else + AssignVariable(change.symbols, derivedSymbols, negatives[j].varname, negatives[j].symbol); + j++; + } + return_value.push_back(change); + add(bitset); + } + return return_value; } /// This absolutely explodes into a billion pieces if the sizeof(a) or b becomes too large. @@ -150,9 +179,9 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons crossProduct.push_back(statechange.first); } else { TTA::StateChange stA{}; - AssignVariable(stA.symbols, derivedSymbols, a[idx].first, a[idx].second); + AssignVariable(stA.symbols, derivedSymbols, a[idx].varname, a[idx].symbol); TTA::StateChange stB{}; - AssignVariable(stB.symbols, derivedSymbols, b[idx].first, b[idx].second); + AssignVariable(stB.symbols, derivedSymbols, b[idx].varname, b[idx].symbol); frontier.push(std::make_pair(curr + stA, idx+1)); frontier.push(std::make_pair(curr + stB, idx+1)); } @@ -164,38 +193,31 @@ std::vector TTASuccessorGenerator::GetNextTockStates(const TTA // Get all the interesting variable predicates auto interestingVarPredicates = GetInterestingVariablePredicatesInState(ttaState); if(interestingVarPredicates.empty()) return {}; - VariableValueCollection positives{}; - VariableValueCollection negatives{}; - for (auto &predicate : interestingVarPredicates) { - auto pos = std::make_pair(predicate.variable, predicate.GetValueOverTheEdge()); - if(negatives.find(pos) == negatives.end()) - positives.insert(pos); - - auto neg = std::make_pair(predicate.variable, predicate.GetValueOnTheEdge()); - if(positives.find(neg) == positives.end()) - negatives.insert(neg); + VariableValueVector positives{}; + VariableValueVector negatives{}; + for (auto& predicate : interestingVarPredicates) { + positives.emplace_back(predicate.variable, predicate.GetValueOverTheEdge()); + negatives.emplace_back(predicate.variable, predicate.GetValueOnTheEdge()); } int limit = -1; + auto size = interestingVarPredicates.size(); if(CLIConfig::getInstance()["explosion-limit"]) limit = CLIConfig::getInstance()["explosion-limit"].as_integer(); spdlog::trace("Size of the set of interesting changes is {0}, this means you will get {1} new states", - positives.size(), static_cast(pow(2, positives.size()))); - if(positives.size() < limit || limit == -1) { - VariableValueVector ps{positives.begin(), positives.end()}; - VariableValueVector ns{negatives.begin(), negatives.end()}; - return BFSCrossProduct(ps, ns, ttaState.GetSymbols()); - } + size, static_cast(pow(2, size))); + if(size < limit || limit == -1) + return SymbolsCrossProduct(positives, negatives, size, ttaState.GetSymbols()); spdlog::warn("The Tock explosion was too large, trying a weaker strategy - This will likely result in wrong answers."); // TODO: This is technically incorrect. These state changes may have an effect on the reachable state space if they are applied together std::vector allChanges{}; for(auto& positive : positives) { TTA::StateChange stP{}; // Positive path - AssignVariable(stP.symbols, ttaState.GetSymbols(), positive.first, positive.second); + AssignVariable(stP.symbols, ttaState.GetSymbols(), positive.varname, positive.symbol); allChanges.push_back(stP); } for(auto& negative : negatives) { TTA::StateChange stN{}; // Negative path - AssignVariable(stN.symbols, ttaState.GetSymbols(), negative.first, negative.second); + AssignVariable(stN.symbols, ttaState.GetSymbols(), negative.varname, negative.symbol); allChanges.push_back(stN); } spdlog::trace("Amount of Tock changes: {0}", allChanges.size()); From cda4ea0e144edd6530e5dfb68cb658ca4a661b39 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 21:05:01 +0200 Subject: [PATCH 15/16] wip --- src/verifier/ReachabilitySearcher.cpp | 4 +++- src/verifier/TTASuccessorGenerator.cpp | 8 +++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index 9f4cc6cd..2c902ca5 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -334,8 +334,10 @@ bool ReachabilitySearcher::AreQueriesAnswered(const std::vector } bool ReachabilitySearcher::IsSearchStateTockable(const SearchState& state) { - return (!state.justTocked && !state.tta.IsCurrentStateImmediate()); + return !state.justTocked + && !state.tta.IsCurrentStateImmediate(); } + #include std::random_device r; ReachabilitySearcher::StateList::iterator ReachabilitySearcher::PickStateFromWaitingList(const nondeterminism_strategy_t& strategy) { diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index 189ed22d..ce9eae5a 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -146,7 +146,8 @@ std::vector SymbolsCrossProduct(const VariableValueVector& pos const TTA::SymbolMap& derivedSymbols) { std::vector return_value{}; std::vector bitset(predicate_count); - for(auto i = 0; i < pow(2, predicate_count); i++) { + auto size = pow(2, predicate_count); + for(auto i = 0; i < size; i++) { TTA::StateChange change{}; auto j = 0; for(auto b : bitset) { @@ -189,10 +190,11 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons return crossProduct; } -std::vector TTASuccessorGenerator::GetNextTockStates(const TTA &ttaState) { +std::vector TTASuccessorGenerator::GetNextTockStates(const TTA& ttaState) { // Get all the interesting variable predicates auto interestingVarPredicates = GetInterestingVariablePredicatesInState(ttaState); - if(interestingVarPredicates.empty()) return {}; + if(interestingVarPredicates.empty()) + return {}; VariableValueVector positives{}; VariableValueVector negatives{}; for (auto& predicate : interestingVarPredicates) { From 7fa2f3d76314204cc9c2c50e96ccdfc192d41513 Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Thu, 21 Apr 2022 21:23:52 +0200 Subject: [PATCH 16/16] Actually found an error in a test model! --- .../Main\342\202\254FischerA\303\2601\304\221.json" | 10 ++++++++++ .../Main\342\202\254FischerB\303\2602\304\221.json" | 10 ++++++++++ 2 files changed, 20 insertions(+) diff --git "a/test/verification/fischer-2/Main\342\202\254FischerA\303\2601\304\221.json" "b/test/verification/fischer-2/Main\342\202\254FischerA\303\2601\304\221.json" index 9f7f086c..24423c8f 100644 --- "a/test/verification/fischer-2/Main\342\202\254FischerA\303\2601\304\221.json" +++ "b/test/verification/fischer-2/Main\342\202\254FischerA\303\2601\304\221.json" @@ -96,6 +96,16 @@ [], "edges": [ + { + "source_location": "Main€FischerAð1đ€L4", + "target_location": "Main€FischerAð1đ€L3", + "select": "", + "guard": "x > k", + "update": "", + "sync": "", + "nails": + [] + }, { "source_location": "Main€FischerAð1đ€L2", "target_location": "Main€FischerAð1đ€L3", diff --git "a/test/verification/fischer-2/Main\342\202\254FischerB\303\2602\304\221.json" "b/test/verification/fischer-2/Main\342\202\254FischerB\303\2602\304\221.json" index 9dcb6b44..3eaabf2e 100644 --- "a/test/verification/fischer-2/Main\342\202\254FischerB\303\2602\304\221.json" +++ "b/test/verification/fischer-2/Main\342\202\254FischerB\303\2602\304\221.json" @@ -96,6 +96,16 @@ [], "edges": [ + { + "source_location": "Main€FischerBð2đ€L4", + "target_location": "Main€FischerBð2đ€L3", + "select": "", + "guard": "x > k", + "update": "", + "sync": "", + "nails": + [] + }, { "source_location": "Main€FischerBð2đ€L2", "target_location": "Main€FischerBð2đ€L3",