Skip to content

Commit

Permalink
Merge pull request #34 from sillydan1/patch/bugfixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@sillydan1
sillydan1 authored Apr 21, 2022
2 parents cfe2a4a + 7fa2f3d commit dca1412
Show file tree
Hide file tree
Showing 9 changed files with 210 additions and 73 deletions.
2 changes: 1 addition & 1 deletion CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 6 additions & 0 deletions src/cli/CLIConfig.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"} },
Expand Down Expand Up @@ -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;
}
Expand Down
1 change: 1 addition & 0 deletions src/model_parsers/TTAParser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ std::vector<std::string> 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) {
Expand Down
70 changes: 48 additions & 22 deletions src/runtime/TTA.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,11 +22,35 @@
#include <tinytimer/Timer.hpp>
#include <verifier/trace_output/TTAResugarizer.h>

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) {
Expand Down Expand Up @@ -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<const std::string, packToken> &symbol,
const std::map<std::string, packToken>::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 {
Expand Down Expand Up @@ -305,8 +327,12 @@ std::string TTA::GetCurrentStateString() const {
std::stringstream ss{}; ss << "{";
for(auto& component : components)
ss<<"\""<<component.first<<"\""<<": "<<"\""<<component.second.currentLocation.identifier<<"\",";
for(auto& symbol : symbols.map())
ss<<"\""<<symbol.first<<"\""<<": "<<"\""<<symbol.second.str()<<"\",";
for(auto& symbol : symbols.map()) {
if(symbol.second->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();
}
Expand Down
3 changes: 3 additions & 0 deletions src/runtime/TTA.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,9 @@ struct TTA {
TokenMap GetSymbolChangesAsMap(std::vector<UpdateExpression> &symbolChanges) const;
void WarnAboutComponentOverlap(component_overlap_t& overlappingComponents) const;
bool TypeCheck(const std::pair<const std::string, packToken> &symbol, const std::map<std::string, packToken>::iterator &changingSymbol) const;
/// WARNING: Very expensive operation!
auto operator==(const TTA& other) -> bool;
auto operator!=(const TTA& other) -> bool;
};

struct StateMultiChoice {
Expand Down
99 changes: 73 additions & 26 deletions src/verifier/ReachabilitySearcher.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,17 +74,19 @@ bool ReachabilitySearcher::IsQuerySatisfied(const Query& query, const TTA &state
}

void ReachabilitySearcher::AreQueriesSatisfied(std::vector<QueryResultPair>& 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});
}
}

Expand Down Expand Up @@ -117,8 +119,21 @@ auto ReachabilitySearcher::PrintResults(const std::vector<QueryResultPair>& 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.");
Expand All @@ -127,10 +142,6 @@ auto ReachabilitySearcher::PrintResults(const std::vector<QueryResultPair>& 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;
Expand Down Expand Up @@ -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<unsigned int> 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)
Expand All @@ -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);
Expand Down Expand Up @@ -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;
}
}
}
}
}
Expand All @@ -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;
}
}
}
}
}
Expand All @@ -293,9 +334,12 @@ bool ReachabilitySearcher::AreQueriesAnswered(const std::vector<QueryResultPair>
}

bool ReachabilitySearcher::IsSearchStateTockable(const SearchState& state) {
return (!state.justTocked && !state.tta.IsCurrentStateImmediate());
return !state.justTocked
&& !state.tta.IsCurrentStateImmediate();
}

#include <random>
std::random_device r;
ReachabilitySearcher::StateList::iterator ReachabilitySearcher::PickStateFromWaitingList(const nondeterminism_strategy_t& strategy) {
if(Waiting.empty())
return Waiting.end();
Expand All @@ -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<size_t> 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;
}
Expand Down
Loading

0 comments on commit dca1412

Please sign in to comment.