diff --git a/src/runtime/TTA.cpp b/src/runtime/TTA.cpp index 7535376d..92cac694 100644 --- a/src/runtime/TTA.cpp +++ b/src/runtime/TTA.cpp @@ -39,6 +39,34 @@ TTA operator<<(const TTA& aa, const TTA::StateChange& b) { return a; } +#define FUNC_IMPL(a, func, b, res) std::visit(overload{[&b,&res](auto&& x){std::visit(overload{[&x,&res](auto&& y){res = func(x,y);}}, static_cast(b));}}, static_cast(a)) +template +auto t_ee(const T1&, const T2&) { + return false; +} +auto t_ee(const bool& a, const bool& b) {return a == b;} +auto t_ee(const int& a, const int& b) {return a == b;} +auto t_ee(const long& a, const long& b) {return a == b;} +auto t_ee(const int& a, const long& b) {return a == b;} +auto t_ee(const long& a, const int& b) {return a == b;} +auto t_ee(const int& a, const float& b) {return a == b;} +auto t_ee(const long& a, const float& b) {return a == b;} +auto t_ee(const float& a, const int& b) {return a == b;} +auto t_ee(const float& a, const long& b) {return a == b;} +auto t_ee(const float& a, const float& b) {return a == b;} +auto t_ee(const TTATimerSymbol& a, const TTATimerSymbol& b) {return a.current_value == b.current_value;} +auto t_ee(const std::string& a, const std::string& b) {return a == b;} +bool operator==(const TTASymbol_t& a, const TTASymbol_t& b) { + bool retVal = a.index() == b.index(); + if(!retVal) + return false; + FUNC_IMPL(a, t_ee, b, retVal); + return retVal; +} +bool operator!=(const TTASymbol_t& a, const TTASymbol_t& b) { + return !(a == b); +} + TTASymbol_t TTASymbolValueFromTypeAndValueStrings(const std::string& typestr, const std::string& valuestr) { return PopulateValueFromString(TTASymbolTypeFromString(typestr), valuestr); } @@ -178,6 +206,8 @@ std::optional TTA::GetChangesFromEdge(const TTA::Edge& choice, changes.component = currentComponent; bool DoesUpdateInfluenceOverlap = AccumulateUpdateInfluences(choice, changes.symbolsToChange, overlappingComponents, currentComponent); outInfluenceOverlap |= DoesUpdateInfluenceOverlap; + if(DoesUpdateInfluenceOverlap) + return {}; for(auto& symbolChange : changes.symbolsToChange) changes.symbolChanges.push_back(symbolChange.second); @@ -186,13 +216,23 @@ std::optional TTA::GetChangesFromEdge(const TTA::Edge& choice, } void TTA::WarnAboutComponentOverlap(component_overlap_t& overlappingComponents) const { - spdlog::debug("Overlapping Components: (Tick#: {0})", tickCount); - for (auto& componentCollection : overlappingComponents) { - if (componentCollection.second.updates.size() > 1) { - for (auto& compname : componentCollection.second.updates) - spdlog::debug("{0}", compname.first); - } + std::vector overlapping_errors{}; + for(auto it = overlappingComponents.begin(), end = overlappingComponents.end(); it != end; it = overlappingComponents.equal_range(it->first).second) { + auto iter = overlappingComponents.equal_range(it->first); + const std::string& compName = iter.first->second.componentName; + for(auto& x = iter.first; x != iter.second; x++) { + if(x->second.componentName != compName) { + overlapping_errors.emplace_back(x->second.componentName + " and " + compName + " disagree on: " + it->first); + break; + } + } } + if(overlapping_errors.empty()) + return; + + spdlog::trace("Overlapping Updates:"); + for(auto& err : overlapping_errors) + spdlog::trace(err); } TokenMap TTA::GetSymbolChangesAsMap(std::vector &symbolChanges) const { @@ -226,29 +266,11 @@ std::vector TTA::GetNextTickStates(const nondeterminism_strate auto enabledEdges = component.second.GetEnabledEdges(symbols); // TODO: Take Interesting variables into account if(!enabledEdges.empty()) { bool hasNondeterminism = WarnIfNondeterminism(enabledEdges, component.first); - if(!hasNondeterminism) { - // Simply pick the edge and apply it to the shared changes - if(strategy != nondeterminism_strategy_t::VERIFICATION) { - auto &pickedEdge = PickEdge(enabledEdges, strategy); - auto changes = GetChangesFromEdge(pickedEdge, updateInfluenceOverlapGlobal, overlappingComponents, component.first); - if (changes.has_value()) sharedChanges.Merge(changes.value()); - ApplyComponentLocation(sharedChanges.currentLocations, component, pickedEdge); - } else { - for(auto& edge : enabledEdges) { - auto changes = GetChangesFromEdge(edge, updateInfluenceOverlapGlobal, overlappingComponents, component.first); - if(changes.has_value()) { - sharedChanges.Merge(changes.value()); - ApplyComponentLocation(sharedChanges.currentLocations, component, edge); - } - } - } - } else { - for(auto& edge : enabledEdges) { - auto changes = GetChangesFromEdge(edge, updateInfluenceOverlapGlobal, overlappingComponents, component.first); - if(changes.has_value()) { - ApplyComponentLocation(changes->currentLocations, component, edge); - choiceChanges.push_back(changes.value()); - } + for(auto& edge : enabledEdges) { + auto changes = GetChangesFromEdge(edge, updateInfluenceOverlapGlobal, overlappingComponents, component.first); + if(changes.has_value()) { + ApplyComponentLocation(changes->currentLocations, component, edge); + choiceChanges.push_back(changes.value()); } } } @@ -281,8 +303,10 @@ bool TTA::WarnIfNondeterminism(const std::vector& edges, const std::string std::string TTA::GetCurrentStateString() const { std::stringstream ss{}; ss << "{"; - for(auto& component : components) ss<<"\""<& symbolsToChange, component_overlap_t& overlappingComponents, const std::string& currentComponent) const { bool updateInfluenceOverlap = false; for(auto& expr : pickedEdge.updateExpressions) { + bool overlap_in_this_expr = false; auto it = overlappingComponents.find(expr.lhs); if(it != overlappingComponents.end()) { auto range = overlappingComponents.equal_range(expr.lhs); for(auto iter = range.first; iter != range.second; iter++) { - if(iter->second.componentName == currentComponent) { - symbolsToChange.insert({ expr.lhs, expr }); + if(iter->second.componentName == currentComponent) continue; - } - // TODO: Check for Indempotence! + // TODO: Check for Idempotence! spdlog::debug("Overlapping update influence on evaluation of update on edge {0} --> {1}. " "Variable '{2}' is already being written to in this tick! - For more info, run with higher verbosity", TTAResugarizer::Resugar(pickedEdge.sourceLocation.identifier), TTAResugarizer::Resugar(pickedEdge.targetLocation.identifier), TTAResugarizer::Resugar(expr.lhs)); // TODO: Idempotent variable assignment updateInfluenceOverlap = true; + overlap_in_this_expr = true; } } component_overlap c{ @@ -410,6 +434,8 @@ bool TTA::AccumulateUpdateInfluences(const TTA::Edge& pickedEdge, std::multimap< pickedEdge.targetLocation.identifier), expr.rhs)} }; overlappingComponents.emplace(expr.lhs, std::move(c)); + if(overlap_in_this_expr) + continue; symbolsToChange.insert({ expr.lhs, expr }); } return updateInfluenceOverlap; diff --git a/src/runtime/TTA.h b/src/runtime/TTA.h index 8224c344..f93a09ad 100644 --- a/src/runtime/TTA.h +++ b/src/runtime/TTA.h @@ -72,7 +72,12 @@ struct TTA { std::vector GetEnabledEdges(const SymbolMap& symbolMap) const; }; + +#ifndef NDEBUG + using ComponentMap = std::map; +#else using ComponentMap = std::unordered_map; +#endif using ComponentLocationMap = std::unordered_map; struct StateChange { ComponentLocationMap componentLocations; diff --git a/src/runtime/TTASymbol.h b/src/runtime/TTASymbol.h index 341d0c9b..85a024c2 100644 --- a/src/runtime/TTASymbol.h +++ b/src/runtime/TTASymbol.h @@ -21,6 +21,7 @@ #ifndef AALTITOAD_TTASYMBOL_H #define AALTITOAD_TTASYMBOL_H #include +#include "extensions/overload" struct TTATimerSymbol { float current_value; @@ -39,6 +40,9 @@ using TTASymbol_t = std::variant< std::string >; +bool operator==(const TTASymbol_t&, const TTASymbol_t&); +bool operator!=(const TTASymbol_t&, const TTASymbol_t&); + TTASymbol_t TTASymbolValueFromTypeAndValueStrings(const std::string& typestr, const std::string& valuestr); TTASymbol_t TTASymbolTypeFromString(const std::string& typestr); TTASymbol_t PopulateValueFromString(const TTASymbol_t& type, const std::string& valuestr); diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp index 43de41a7..1cbf04d0 100644 --- a/src/verifier/ReachabilitySearcher.cpp +++ b/src/verifier/ReachabilitySearcher.cpp @@ -39,13 +39,11 @@ bool IsQuerySatisfiedHelper(const Query& query, const TTA& state) { case NodeType_t::CompEq: case NodeType_t::CompGreater: case NodeType_t::CompGreaterEq: { - std::string exprstring{}; // This string can technically be precompiled. - query.children[0].tree_apply([&exprstring]( const ASTNode& node ){ exprstring += node.token; }); - exprstring += query.root.token; - query.children[1].tree_apply([&exprstring]( const ASTNode& node ){ exprstring += node.token; }); - spdlog::debug("Assembled expression '{0}'", exprstring); - calculator c(exprstring.c_str()); - return c.eval(state.GetSymbols()).asBool(); + std::stringstream exprstring{}; // This string can technically be precompiled. + query.children[0].tree_apply([&exprstring]( const ASTNode& node ){ exprstring << node.token; }); + exprstring << query.root.token; + query.children[1].tree_apply([&exprstring]( const ASTNode& node ){ exprstring << node.token; }); + return calculator(exprstring.str().c_str()).eval(state.GetSymbols()).asBool(); } case NodeType_t::SubExpr: case NodeType_t::Finally: @@ -66,9 +64,7 @@ bool IsQuerySatisfiedHelper(const Query& query, const TTA& state) { bool ReachabilitySearcher::IsQuerySatisfied(const Query& query, const TTA &state) { if(query.root.type == NodeType_t::Forall && query.children.begin()->root.type == NodeType_t::Globally) { - auto invertedQ = Query(ASTNode{NodeType_t::Negation, "!"}); - invertedQ.insert(query); - return IsQuerySatisfiedHelper(invertedQ, state); + return !IsQuerySatisfiedHelper(query, state); } if(query.root.type != NodeType_t::Exists) { spdlog::critical("Only reachability queries are supported right now, sorry."); @@ -96,17 +92,22 @@ void ReachabilitySearcher::OutputResults(const std::vector& res if(CLIConfig::getInstance()["output"]) { std::ofstream outputFile{CLIConfig::getInstance()["output"].as_string(), std::ofstream::trunc}; for(auto& r : results) { - outputFile << ConvertASTToString(*r.query) << " : " << std::boolalpha << r.answer << "\n"; + auto answer = r.query->root.type == NodeType_t::Forall && r.query->children[0].root.type == NodeType_t::Globally ? !r.answer : r.answer; + outputFile << ConvertASTToString(*r.query) << " : " << std::boolalpha << answer << "\n"; } } } -void ReachabilitySearcher::PrintResults(const std::vector& results) { +auto ReachabilitySearcher::PrintResults(const std::vector& results) -> int { OutputResults(results); + auto acceptedResults = 0; spdlog::info("==== QUERY RESULTS ===="); for(const auto& r : results) { spdlog::info("===================="); // Delimiter to make it easier to read - spdlog::info("{0} : {1}", ConvertASTToString(*r.query), r.answer); + auto answer = r.query->root.type == NodeType_t::Forall && r.query->children[0].root.type == NodeType_t::Globally ? !r.answer : r.answer; + if(answer) + acceptedResults++; + spdlog::info("{0} : {1}", ConvertASTToString(*r.query), answer); auto stateHash = r.acceptingStateHash; auto state = r.acceptingState; std::vector trace{}; @@ -135,13 +136,18 @@ void ReachabilitySearcher::PrintResults(const std::vector& resu break; } } + if(trace.empty()) { + spdlog::info("No trace available"); + continue; + } spdlog::info("Trace:"); std::reverse(trace.begin(), trace.end()); - printf("["); + printf("[\n"); for(auto& stateStr : trace) printf("%s,\n", stateStr.c_str()); printf("]\n"); } + return acceptedResults; } auto debug_int_as_hex_str(size_t v) { @@ -150,17 +156,32 @@ auto debug_int_as_hex_str(size_t v) { return std::string(buffer); } +std::string debug_get_current_state_string_human(const TTA& tta) { + std::stringstream ss{}; + for(auto& c : tta.components) + ss << c.second.currentLocation.identifier << ", "; + return ss.str(); +} + void debug_print_passed_list(const ReachabilitySearcher& r) { spdlog::trace("==== PASSED LIST ===="); for(auto& e : r.Passed) { - spdlog::trace("Hash:{0} Prev:{1}", + if(e.first == e.second.prevStateHash) { + spdlog::warn("Hash:{0} Prev:{1} \tState:{2}", + debug_int_as_hex_str(e.first), + debug_int_as_hex_str(e.second.prevStateHash), + debug_get_current_state_string_human(e.second.tta)); + continue; + } + spdlog::trace("Hash:{0} Prev:{1} \tState:{2}", debug_int_as_hex_str(e.first), - debug_int_as_hex_str(e.second.prevStateHash)); + debug_int_as_hex_str(e.second.prevStateHash), + debug_get_current_state_string_human(e.second.tta)); } spdlog::trace("====/PASSED LIST ===="); } -void debug_cleanup_waiting_list(ReachabilitySearcher& s, size_t curstatehash, const SearchState& state) { +void cleanup_waiting_list(ReachabilitySearcher& s, size_t curstatehash, const SearchState& state) { bool found; do { found = false; @@ -175,6 +196,13 @@ void debug_cleanup_waiting_list(ReachabilitySearcher& s, size_t curstatehash, co } while(found); } +std::string debug_get_symbol_map_string_representation(const TTA::SymbolMap& map) { + std::ostringstream ss{}; + for(auto& symbol : map.map()) + ss << symbol.first << " :-> " << symbol.second << ", "; + return ss.str(); +} + bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strategy_t& strategy) { auto stateit = Waiting.begin(); while(stateit != Waiting.end()) { @@ -183,9 +211,11 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate AreQueriesSatisfied(query_results, state.tta, curstatehash); if(AreQueriesAnswered(query_results)) { Passed.emplace(std::make_pair(curstatehash, state)); - if(!CLIConfig::getInstance()["notrace"]) - PrintResults(query_results); + if(CLIConfig::getInstance()["verbosity"] && CLIConfig::getInstance()["verbosity"].as_integer() >= 6) + debug_print_passed_list(*this); spdlog::info("Found a positive result after searching: {0} states", Passed.size()); + if(!CLIConfig::getInstance()["notrace"]) + return query_results.size() - PrintResults(query_results) == 0; return true; // All the queries has been reached } // If the state is interesting, apply tock changes @@ -198,14 +228,15 @@ bool ReachabilitySearcher::ForwardReachabilitySearch(const nondeterminism_strate AddToWaitingList(state.tta, allTickStateChanges, false, curstatehash); Passed.emplace(std::make_pair(curstatehash, state)); - debug_cleanup_waiting_list(*this, curstatehash, state); + + cleanup_waiting_list(*this, curstatehash, state); stateit = PickStateFromWaitingList(strategy); } - if(!CLIConfig::getInstance()["notrace"]) - PrintResults(query_results); spdlog::info("Found a negative result after searching: {0} states", Passed.size()); if(CLIConfig::getInstance()["verbosity"].as_integer() >= 6) debug_print_passed_list(*this); + if(!CLIConfig::getInstance()["notrace"]) + return query_results.size() - PrintResults(query_results) == 0; return false; } @@ -228,8 +259,10 @@ void ReachabilitySearcher::AddToWaitingList(const TTA &state, const std::vector< auto nstate = state << change; auto nstatehash = nstate.GetCurrentStateHash(); if (Passed.find(nstatehash) == Passed.end()) { - if (nstatehash == state_hash) - spdlog::warn("Colliding state hashes!"); + if (nstatehash == state_hash) { + spdlog::warn("Recursive state hashes!"); + continue; + } Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked})); } } @@ -238,12 +271,16 @@ void ReachabilitySearcher::AddToWaitingList(const TTA &state, const std::vector< if(statechanges.size() > 1) { auto baseChanges = state << *statechanges.begin(); for (auto it = statechanges.begin() + 1; it != statechanges.end(); ++it) { + if(it->IsEmpty()) + continue; /// 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()) { - if (nstatehash == state_hash) - spdlog::warn("Colliding state hashes!"); + if (nstatehash == state_hash) { + spdlog::warn("Recursive state hashes!"); + continue; + } Waiting.emplace(std::make_pair(nstatehash, SearchState{nstate, state_hash, justTocked})); } } diff --git a/src/verifier/ReachabilitySearcher.h b/src/verifier/ReachabilitySearcher.h index a09f336c..efce63fe 100644 --- a/src/verifier/ReachabilitySearcher.h +++ b/src/verifier/ReachabilitySearcher.h @@ -55,7 +55,7 @@ struct ReachabilitySearcher { bool IsQuerySatisfied(const Query& query, const TTA& state); void AreQueriesSatisfied(std::vector& queries, const TTA& state, size_t state_hash); bool ForwardReachabilitySearch(const nondeterminism_strategy_t& strategy); - void PrintResults(const std::vector& results); + auto PrintResults(const std::vector& results) -> int; void OutputResults(const std::vector& results); StateList::iterator PickStateFromWaitingList(const nondeterminism_strategy_t& strategy); }; diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp index 9b58d503..90ef76f8 100644 --- a/src/verifier/TTASuccessorGenerator.cpp +++ b/src/verifier/TTASuccessorGenerator.cpp @@ -157,18 +157,23 @@ std::vector TTASuccessorGenerator::GetNextTockStates(const TTA VariableValueCollection positives{}; VariableValueCollection negatives{}; for (auto &predicate : interestingVarPredicates) { - positives.insert(std::make_pair(predicate.variable, predicate.GetValueOverTheEdge())); - negatives.insert(std::make_pair(predicate.variable, predicate.GetValueOnTheEdge())); + 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); } int limit = -1; - if(CLIConfig::getInstance()["explosion-limit"]) limit = CLIConfig::getInstance()["explosion-limit"].as_integer(); + 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(limit == -1 || positives.size() < limit) { + if(positives.size() < limit || limit == -1) { VariableValueVector ps{positives.begin(), positives.end()}; VariableValueVector ns{negatives.begin(), negatives.end()}; - std::vector allPermutations = BFSCrossProduct(ps, ns, ttaState.GetSymbols()); - return allPermutations; + return BFSCrossProduct(ps, ns, 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 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 2fbd82af..9f7f086c 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" @@ -1 +1,168 @@ -{"name":"Main€FischerAð1đ","declarations":"","locations":[{"id":"Main€FischerAð1đ€L3","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},{"id":"Main€FischerAð1đ€L4","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},{"id":"Main€FischerAð1đ€L5","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},{"id":"Main€FischerAð1đ€L6","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0}],"initial_location": {"id":"Main€FischerAð1đ€L2","nickname":"","invariant":"","type":"INITIAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},"final_location": {"id":"Main€FischerAð1đ€L8","nickname":"","invariant":"","type":"FINAl","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},"jorks":[],"sub_components": [],"edges": [{"source_location": "Main€FischerAð1đ€L2","target_location": "Main€FischerAð1đ€L3","select":"","guard":"true","update":"","sync":"","nails": []},{"source_location": "Main€FischerAð1đ€L3","target_location": "Main€FischerAð1đ€L4","select":"","guard":"pubid == 0","update":"x := 0;","sync":"","nails": []},{"source_location": "Main€FischerAð1đ€L5","target_location": "Main€FischerAð1đ€L6","select":"","guard":"pubid == 1","update":"counter := counter +1 ;x := 0;","sync":"","nails": []},{"source_location": "Main€FischerAð1đ€L4","target_location": "Main€FischerAð1đ€L5","select":"","guard":"x <= k","update":"pubid := 1;","sync":"","nails": []},{"source_location": "Main€FischerAð1đ€L5","target_location": "Main€FischerAð1đ€L4","select":"","guard":"x > k && pubid != 1","update":"x := 0;","sync":"","nails": []},{"source_location": "Main€FischerAð1đ€L6","target_location": "Main€FischerAð1đ€L3","select":"","guard":"true","update":"pubid := 0 ;counter := counter -1;","sync":"","nails": []}],"main":false,"description": "AUTOMATICALLY GENERATED. DO NOT USE THIS","x":0.0,"y":0.0,"width":0.0,"height":0.0,"color":"7","include_in_periodic_check":false} \ No newline at end of file +{ + "name": "Main€FischerAð1đ", + "declarations": "", + "locations": + [ + { + "id": "Main€FischerAð1đ€L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + { + "id": "Main€FischerAð1đ€L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + { + "id": "Main€FischerAð1đ€L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + { + "id": "Main€FischerAð1đ€L6", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + } + ], + "initial_location": + { + "id": "Main€FischerAð1đ€L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + "final_location": + { + "id": "Main€FischerAð1đ€L8", + "nickname": "", + "invariant": "", + "type": "FINAl", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + "jorks": + [], + "sub_components": + [], + "edges": + [ + { + "source_location": "Main€FischerAð1đ€L2", + "target_location": "Main€FischerAð1đ€L3", + "select": "", + "guard": "true", + "update": "", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerAð1đ€L3", + "target_location": "Main€FischerAð1đ€L4", + "select": "", + "guard": "pubid == 0", + "update": "x := 0;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerAð1đ€L5", + "target_location": "Main€FischerAð1đ€L6", + "select": "", + "guard": "pubid == 1 && counter == 0", + "update": "counter := counter +1 ;x := 0;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerAð1đ€L4", + "target_location": "Main€FischerAð1đ€L5", + "select": "", + "guard": "x <= k", + "update": "pubid := 1;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerAð1đ€L5", + "target_location": "Main€FischerAð1đ€L4", + "select": "", + "guard": "x > k && pubid != 1", + "update": "x := 0;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerAð1đ€L6", + "target_location": "Main€FischerAð1đ€L3", + "select": "", + "guard": "true", + "update": "pubid := 0 ;counter := counter -1;", + "sync": "", + "nails": + [] + } + ], + "main": false, + "description": "AUTOMATICALLY GENERATED. DO NOT USE THIS", + "x": 0.0, + "y": 0.0, + "width": 0.0, + "height": 0.0, + "color": "7", + "include_in_periodic_check": false +} \ No newline at end of file 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 125edf42..9dcb6b44 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" @@ -1 +1,168 @@ -{"name":"Main€FischerBð2đ","declarations":"","locations":[{"id":"Main€FischerBð2đ€L3","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},{"id":"Main€FischerBð2đ€L4","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},{"id":"Main€FischerBð2đ€L5","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},{"id":"Main€FischerBð2đ€L6","nickname":"","invariant":"","type":"NORMAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0}],"initial_location": {"id":"Main€FischerBð2đ€L2","nickname":"","invariant":"","type":"INITIAL","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},"final_location": {"id":"Main€FischerBð2đ€L8","nickname":"","invariant":"","type":"FINAl","urgency": "NORMAL","x": 0.0,"y": 0.0,"color": "7","nickname_x": 0.0,"nickname_y": 0.0,"invariant_x":0.0,"invariant_y":0.0},"jorks":[],"sub_components": [],"edges": [{"source_location": "Main€FischerBð2đ€L2","target_location": "Main€FischerBð2đ€L3","select":"","guard":"true","update":"","sync":"","nails": []},{"source_location": "Main€FischerBð2đ€L3","target_location": "Main€FischerBð2đ€L4","select":"","guard":"pubid == 0","update":"x := 0;","sync":"","nails": []},{"source_location": "Main€FischerBð2đ€L5","target_location": "Main€FischerBð2đ€L6","select":"","guard":"pubid == 2","update":"counter := counter +1 ;x := 0;","sync":"","nails": []},{"source_location": "Main€FischerBð2đ€L4","target_location": "Main€FischerBð2đ€L5","select":"","guard":"x <= k","update":"pubid := 2;","sync":"","nails": []},{"source_location": "Main€FischerBð2đ€L5","target_location": "Main€FischerBð2đ€L4","select":"","guard":"x > k && pubid != 2","update":"x := 0;","sync":"","nails": []},{"source_location": "Main€FischerBð2đ€L6","target_location": "Main€FischerBð2đ€L3","select":"","guard":"true","update":"pubid := 0 ;counter := counter -1;","sync":"","nails": []}],"main":false,"description": "AUTOMATICALLY GENERATED. DO NOT USE THIS","x":0.0,"y":0.0,"width":0.0,"height":0.0,"color":"7","include_in_periodic_check":false} \ No newline at end of file +{ + "name": "Main€FischerBð2đ", + "declarations": "", + "locations": + [ + { + "id": "Main€FischerBð2đ€L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + { + "id": "Main€FischerBð2đ€L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + { + "id": "Main€FischerBð2đ€L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + { + "id": "Main€FischerBð2đ€L6", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + } + ], + "initial_location": + { + "id": "Main€FischerBð2đ€L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + "final_location": + { + "id": "Main€FischerBð2đ€L8", + "nickname": "", + "invariant": "", + "type": "FINAl", + "urgency": "NORMAL", + "x": 0.0, + "y": 0.0, + "color": "7", + "nickname_x": 0.0, + "nickname_y": 0.0, + "invariant_x": 0.0, + "invariant_y": 0.0 + }, + "jorks": + [], + "sub_components": + [], + "edges": + [ + { + "source_location": "Main€FischerBð2đ€L2", + "target_location": "Main€FischerBð2đ€L3", + "select": "", + "guard": "true", + "update": "", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerBð2đ€L3", + "target_location": "Main€FischerBð2đ€L4", + "select": "", + "guard": "pubid == 0", + "update": "x := 0;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerBð2đ€L5", + "target_location": "Main€FischerBð2đ€L6", + "select": "", + "guard": "pubid == 2 && counter == 0", + "update": "counter := counter +1 ;x := 0;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerBð2đ€L4", + "target_location": "Main€FischerBð2đ€L5", + "select": "", + "guard": "x <= k", + "update": "pubid := 2;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerBð2đ€L5", + "target_location": "Main€FischerBð2đ€L4", + "select": "", + "guard": "x > k && pubid != 2", + "update": "x := 0;", + "sync": "", + "nails": + [] + }, + { + "source_location": "Main€FischerBð2đ€L6", + "target_location": "Main€FischerBð2đ€L3", + "select": "", + "guard": "true", + "update": "pubid := 0 ;counter := counter -1;", + "sync": "", + "nails": + [] + } + ], + "main": false, + "description": "AUTOMATICALLY GENERATED. DO NOT USE THIS", + "x": 0.0, + "y": 0.0, + "width": 0.0, + "height": 0.0, + "color": "7", + "include_in_periodic_check": false +} \ No newline at end of file diff --git a/test/verification/fischer-2/Queries.json b/test/verification/fischer-2/Queries.json index 16d81b9d..189692d2 100644 --- a/test/verification/fischer-2/Queries.json +++ b/test/verification/fischer-2/Queries.json @@ -1,12 +1,27 @@ [ { - "query": "E F counter \u003d\u003d 1", - "comment": "Can any processes get to CS?", + "query": "A G ! (counter > 1)", + "comment": "", "is_periodic": false }, { - "query": "E F Main€FischerA(1).L6 && Main€FischerB(2).L6", - "comment": "Can both processes get to the critical section at the same time?", + "query": "A G ! (counter < 0)", + "comment": "", + "is_periodic": false + }, + { + "query": "E F counter == 1", + "comment": "", + "is_periodic": false + }, + { + "query": "A G ! deadlock", + "comment": "", + "is_periodic": false + }, + { + "query": "A G !(Main€FischerA(1).L6 && Main€FischerB(2).L6)", + "comment": "", "is_periodic": false } ] \ No newline at end of file diff --git a/test/verification/fischer-2/expected_results.ignore.txt b/test/verification/fischer-2/expected_results.ignore.txt index 181ee28e..7ffd7d6c 100644 --- a/test/verification/fischer-2/expected_results.ignore.txt +++ b/test/verification/fischer-2/expected_results.ignore.txt @@ -1,2 +1,5 @@ +A G ! (counter > 1) : true +A G ! (counter < 0) : true E F counter == 1 : true -E F Main€FischerA(1).L6 && Main€FischerB(2).L6 : true +A G ! deadlock : true +A G ! (Main€FischerA(1).L6 && Main€FischerB(2).L6) : true