From 8dbfb5954eca3b8b505a2e1010b46fad46601b0b Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Fri, 29 Apr 2022 12:59:22 +0200 Subject: [PATCH 1/3] Update to newest argvparse --- dep/argvparse | 2 +- src/cli/CLIConfig.cpp | 1 - src/verifier/ReachabilitySearcher.cpp | 2 +- 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/dep/argvparse b/dep/argvparse index 14c2e60d..8f55f05f 160000 --- a/dep/argvparse +++ b/dep/argvparse @@ -1 +1 @@ -Subproject commit 14c2e60d85176722153631d8d51c355cfeb2f9b8 +Subproject commit 8f55f05fb628e8c07a6c50190a970f3656b021c3 diff --git a/src/cli/CLIConfig.cpp b/src/cli/CLIConfig.cpp index 8d1d97ec..4ff96677 100644 --- a/src/cli/CLIConfig.cpp +++ b/src/cli/CLIConfig.cpp @@ -82,7 +82,6 @@ std::vector CLIConfig::GetCLIOptionsOnly() { std::transform(cliOptions.begin(), cliOptions.end(), std::back_inserter(output), [](std::pair element) -> option_t { return element.second; }); - add_help_option(output); return output; } diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index 2c902ca5..ab791bf9 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -255,7 +255,7 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate stateit = PickStateFromWaitingList(strategy); } spdlog::info("Found a negative result after searching: {0} states", Passed.size()); - if(CLIConfig::getInstance()["verbosity"].as_integer() >= 6) + if(CLIConfig::getInstance()["verbosity"].as_integer_or_default(0) >= 6) debug_print_passed_list(*this); if(!CLIConfig::getInstance()["notrace"]) return query_results.size() - PrintResults(query_results) == 0; From f83b2db0355049f4289c91b0bcdafca273cc828a Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Fri, 29 Apr 2022 12:59:42 +0200 Subject: [PATCH 2/3] Correctly calculate crossproduct for external variables in edges --- src/verifier/TTASuccessorGenerator.cpp | 44 +++++++++++--------------- src/verifier/TTASuccessorGenerator.h | 3 +- 2 files changed, 20 insertions(+), 27 deletions(-) diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index ce9eae5a..f48c70cc 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -25,19 +25,21 @@ std::vector TTASuccessorGenerator::GetNextTickStates(const TTA return tta.GetNextTickStates(nondeterminism_strategy_t::VERIFICATION); } -std::vector TTASuccessorGenerator::GetInterestingVariablePredicatesInState(const TTA &ttaState) { +std::vector> TTASuccessorGenerator::GetInterestingVariablePredicatesInState(const TTA &ttaState) { // Get all edges that we may be able to take. auto currentEdges = ttaState.GetCurrentEdges(); // Filter over the "interesting" edges currentEdges.erase(std::remove_if(currentEdges.begin(), currentEdges.end(), [](const auto& edge){ return !edge.ContainsExternalChecks(); }), currentEdges.end()); // Extract predicates based on the guards of those edges - std::vector preds{}; + std::vector> all_preds{}; for(auto& edge : currentEdges) { + std::vector preds{}; for(auto& expr : edge.externalGuardCollection) preds.push_back(ConvertFromGuardExpression(expr, ttaState)); + all_preds.push_back(preds); } - return preds; // TODO: Check for uniqueness and/or satisfiability + return all_preds; // TODO: Check for uniqueness and/or satisfiability } VariablePredicate TTASuccessorGenerator::ConvertFromGuardExpression(const TTA::GuardExpression &expressionTree, const TTA& ttaState) { @@ -193,35 +195,25 @@ std::vector BFSCrossProduct(const VariableValueVector& a, cons std::vector TTASuccessorGenerator::GetNextTockStates(const TTA& ttaState) { // Get all the interesting variable predicates auto interestingVarPredicates = GetInterestingVariablePredicatesInState(ttaState); - if(interestingVarPredicates.empty()) + std::vector return_value{}; + for(auto& preds : interestingVarPredicates) { + auto changes = GetNextTockStatesFromPredicates(preds, ttaState.GetSymbols()); + return_value.insert(return_value.end(), changes.begin(), changes.end()); + } + return return_value; +} + +std::vector TTASuccessorGenerator::GetNextTockStatesFromPredicates(const std::vector& predicates, const TTA::SymbolMap& symbols) { + if(predicates.empty()) return {}; VariableValueVector positives{}; VariableValueVector negatives{}; - for (auto& predicate : interestingVarPredicates) { + for (auto& predicate : predicates) { 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(); + auto size = predicates.size(); spdlog::trace("Size of the set of interesting changes is {0}, this means you will get {1} new states", 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.varname, positive.symbol); - allChanges.push_back(stP); - } - for(auto& negative : negatives) { - TTA::StateChange stN{}; // Negative path - AssignVariable(stN.symbols, ttaState.GetSymbols(), negative.varname, negative.symbol); - allChanges.push_back(stN); - } - spdlog::trace("Amount of Tock changes: {0}", allChanges.size()); - return allChanges; + return SymbolsCrossProduct(positives, negatives, size, symbols); } diff --git a/src/verifier/TTASuccessorGenerator.h b/src/verifier/TTASuccessorGenerator.h index 822bdbc3..180c579b 100644 --- a/src/verifier/TTASuccessorGenerator.h +++ b/src/verifier/TTASuccessorGenerator.h @@ -26,11 +26,12 @@ class TTASuccessorGenerator { /// Gets the set of states that are reachable in the given state (no tocking implications) static std::vector GetNextTickStates(const TTA& ttaStateAndGraph); /// Gets all the predicates - static std::vector GetInterestingVariablePredicatesInState(const TTA& ttaState); + static std::vector> GetInterestingVariablePredicatesInState(const TTA& ttaState); /// A more efficient way of checking if the state is interesting, than getting an empty vector static bool IsStateInteresting(const TTA& ttaState); /// Finds and applies all available interesting predicates static std::vector GetNextTockStates(const TTA& ttaState); + static std::vector GetNextTockStatesFromPredicates(const std::vector& predicates, const TTA::SymbolMap& symbols); private: static VariablePredicate ConvertFromGuardExpression(const TTA::GuardExpression& expressionTree, const TTA& ttaState); From c8e23a29b06d4ab3aa9cd8872db155af8807744f Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Fri, 29 Apr 2022 13:00:05 +0200 Subject: [PATCH 3/3] Update version to 0.10.1 --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8f18c65a..c4c8f777 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.10.0) +project(aaltitoad VERSION 0.10.1) configure_file(src/config.h.in config.h) set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED)