wip

sillydan1 · Apr 21, 2022 · cda4ea0 · cda4ea0
1 parent 98929da
commit cda4ea0
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/src/verifier/ReachabilitySearcher.cpp b/src/verifier/ReachabilitySearcher.cpp
@@ -334,8 +334,10 @@ 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) {

diff --git a/src/verifier/TTASuccessorGenerator.cpp b/src/verifier/TTASuccessorGenerator.cpp
@@ -146,7 +146,8 @@ std::vector<TTA::StateChange> SymbolsCrossProduct(const VariableValueVector& pos
                                                   const TTA::SymbolMap& derivedSymbols) {
     std::vector<TTA::StateChange> return_value{};
     std::vector<bool> 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<TTA::StateChange> BFSCrossProduct(const VariableValueVector& a, cons
     return crossProduct;
 }
 
-std::vector<TTA::StateChange> TTASuccessorGenerator::GetNextTockStates(const TTA &ttaState) {
+std::vector<TTA::StateChange> 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) {