Merge pull request #55 from MortenSchou/weight-for-trace

Query weight notation for trace and rules

Author: petergjoel

CMakeLists.txt

@@ -51,7 +51,7 @@ if (AALWINES_GetDependencies)
     )
     ExternalProject_add(pdaaal-ext
         GIT_REPOSITORY [email protected]:DEIS-Tools/PDAAAL.git
-        GIT_TAG 99d9622646c9c6122548277f9c944380fe775de5
+        GIT_TAG e205e51be36cd32312739be61c552aa46fb31761
         #URL https://github.com/DEIS-Tools/PDAAAL/archive/v0.2.1.zip
         #URL_HASH SHA512=f6f49a6d4cbb5fda1ac173fa77fe1eb1436ffe4112cc6f8fabdd8c879fad1aa90aa6be20804d5777bbfff902dd800f9f66dd1afb808d014653e21722dcb91b87
         CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION} -DPDAAAL_BuildTests=OFF -DCMAKE_BUILD_TYPE=Release -DPTRIE_INSTALL_DIR=${EXTERNAL_INSTALL_LOCATION}/include

src/aalwines/model/NetworkPDAFactory.h

@@ -387,9 +387,6 @@ namespace aalwines {
                 auto eid = ((&entry) - s._inf->table().entries().data());
                 auto rid = ((&forward) - entry._rules.data());
                 res = add_state(n, s._inf, appmode, eid, rid, 0);
-                if constexpr (is_weighted) {
-                    ar._weight = _weight_f(forward, false);
-                }
             }
             ar._dest = res.second;
 
@@ -481,17 +478,14 @@ namespace aalwines {
             } else {
                 auto res = add_state(s._nfastate, s._inf, s._appmode, s._eid, s._rid, s._opid + 1);
                 nr._dest = res.second;
-                if constexpr (is_weighted) {
-                    nr._weight = _weight_f(r, false);
-                }
             }
             //or/andHere
         }
         return result;
     }
 
     template<typename W_FN, typename W>
-    void NetworkPDAFactory<W_FN, W>::print_trace_rule(std::ostream &stream, const Interface* inf, 
+    void NetworkPDAFactory<W_FN, W>::print_trace_rule(std::ostream &stream, const Interface* inf,
                                                   const RoutingTable::entry_t &entry,
                                                   const RoutingTable::forward_t &rule) const {
         stream << "{";
@@ -509,6 +503,16 @@ namespace aalwines {
         }
         stream << ",\"rule\":";
         rule.print_json(stream, false);
+
+        if constexpr (is_weighted) {
+            stream << ", \"priority-weight\": [";
+            auto weights = _weight_f(rule, true);
+            for (size_t v = 0; v < weights.size(); v++){
+                if (v != 0) stream << ", ";
+                stream << "\"" << std::to_string(weights[v]) << "\"";
+            }
+            stream << "]";
+        }
         stream << "}";
     }
 

src/main.cpp

@@ -54,13 +54,12 @@ bool do_verification(stopwatch& compilation_time, stopwatch& reduction_time, sto
         Query& q, Query::mode_t m, Network& network, bool no_ip_swap, std::pair<size_t,size_t>& reduction, size_t tos,
         bool need_trace, size_t engine, Moped& moped, SolverAdapter& solver, utils::outcome_t& result,
         std::vector<pdaaal::TypedPDA<Query::label_t>::tracestate_t >& trace, std::stringstream& proof,
-        const W_FN& weight_fn) {
+        std::vector<unsigned int>& trace_weight, const W_FN& weight_fn) {
     compilation_time.start();
     q.set_approximation(m);
     NetworkPDAFactory factory(q, network, no_ip_swap, weight_fn);
     auto pda = factory.compile();
     compilation_time.stop();
-
     reduction_time.start();
     reduction = Reducer::reduce(pda, tos, pda.initial(), pda.terminal());
     reduction_time.stop();
@@ -88,7 +87,11 @@ bool do_verification(stopwatch& compilation_time, stopwatch& reduction_time, sto
             engine_outcome = solver_result.first;
             verification_time.stop();
             if (need_trace && engine_outcome) {
-                trace = solver.get_trace(pda, std::move(solver_result.second));
+                if constexpr (pdaaal::is_weighted<typename W_FN::result_type>) {
+                    std::tie(trace, trace_weight) = solver.get_trace<pdaaal::Trace_Type::Shortest>(pda, std::move(solver_result.second));
+                } else {
+                    trace = solver.get_trace<pdaaal::Trace_Type::Any>(pda, std::move(solver_result.second));
+                }
                 if (factory.write_json_trace(proof, trace))
                     result = utils::YES;
             }
@@ -374,18 +377,19 @@ int main(int argc, const char** argv)
             stopwatch reduction_time(false);
             stopwatch verification_time(false);
             std::vector<pdaaal::TypedPDA<Query::label_t>::tracestate_t > trace;
+            std::vector<unsigned int> trace_weight;
             std::stringstream proof;
             bool need_trace = was_dual || get_trace;
             for(auto m : modes) {
                 bool engine_outcome;
                 if (weight_fn) {
                     engine_outcome = do_verification(compilation_time, reduction_time,
                             verification_time,q, m, network, no_ip_swap, reduction, tos, need_trace, engine,
-                            moped, solver,result, trace, proof, weight_fn.value());
+                            moped, solver,result, trace, proof, trace_weight, weight_fn.value());
                 } else {
                     engine_outcome = do_verification<std::function<void(void)>>(compilation_time, reduction_time,
                             verification_time,q, m,network, no_ip_swap, reduction, tos, need_trace, engine,
-                            moped, solver,result, trace, proof, [](){});
+                            moped, solver,result, trace, proof, trace_weight, [](){});
                 }
                 if(q.number_of_failures() == 0)
                     result = engine_outcome ? utils::YES : utils::NO;
@@ -416,11 +420,19 @@ int main(int argc, const char** argv)
                 break;
             }
             std::cout << ",\n";
-            std::cout << "\t\t\"engine\":" << engineTypes[engine] << ", " << std::endl;
-            std::cout << "\t\t\"mode\":" << modeTypes[mode] << ", " << std::endl;
+            std::cout << "\t\t\"engine\": \"" << engineTypes[engine] << "\", " << std::endl;
+            std::cout << "\t\t\"mode\": \"" << modeTypes[mode] << "\", " << std::endl;
             std::cout << "\t\t\"reduction\":[" << reduction.first << ", " << reduction.second << "]";
             if(get_trace && result == utils::YES)
             {
+                if(weight_fn) {
+                    std::cout << ",\n\t\t\"trace-weight\": [";
+                    for(size_t i = 0; i < trace_weight.size(); i++){
+                        if(i != 0) std::cout << ", ";
+                        std::cout << trace_weight[i];
+                    }
+                    std::cout << "]";
+                }
                 std::cout << ",\n\t\t\"trace\":[\n";
                 std::cout << proof.str();
                 std::cout << "\n\t\t]";