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) diff --git a/src/cli/CLIConfig.cpp b/src/cli/CLIConfig.cpp index c40caf56..8d1d97ec 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"} }, @@ -60,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/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) { diff --git a/src/runtime/TTA.cpp b/src/runtime/TTA.cpp index 92cac694..9a42d120 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) { @@ -168,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 { @@ -305,8 +327,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(); } 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/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index fd1b313e..2c902ca5 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -74,17 +74,19 @@ 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()); - } - } + for(auto& query : queries) { + 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}); } } @@ -117,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."); @@ -127,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; @@ -206,10 +217,19 @@ 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; - 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 +249,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); @@ -259,12 +280,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; + } + } } } } @@ -277,12 +308,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; + } + } } } } @@ -293,9 +334,12 @@ 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) { if(Waiting.empty()) return Waiting.end(); @@ -309,14 +353,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; } diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index 90ef76f8..ce9eae5a 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( @@ -123,6 +129,40 @@ void AssignVariable(TTA::SymbolMap& outputMap, const TTA::SymbolMap& currentValu [&](const std::string& v) { outputMap.map()[varname] = v; } ), newValue); } + +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); + auto size = pow(2, predicate_count); + for(auto i = 0; i < size; 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. /// i.e. just 16 changes equals 65536 stateChanges (2^N) /// - which is not something that doesnt happen @@ -136,13 +176,13 @@ 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{}; - 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, a[idx].first, a[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)); } @@ -150,42 +190,36 @@ 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 {}; - 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); + if(interestingVarPredicates.empty()) + return {}; + 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()); 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",