diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 214bf0250..78e665fb6 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -49,13 +49,14 @@ static const argp_option options[] = { /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL, + { "dot", OPT_DOT, "a|c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters for " "(a) acceptance display, (c) circular nodes, (h) horizontal layout, " "(v) vertical layout, (n) with name, (N) without name, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, - { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " + "(i) use implicit labels for complete deterministic automata, " "(s) prefer state-based acceptance when possible [default], " "(t) force transition-based acceptance, " "(m) mix state and transition-based acceptance, " diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 15d41ae55..f518e0c59 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -71,13 +71,14 @@ static const argp_option options[] = "of the given property)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL, + { "dot", OPT_DOT, "a|c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters for (a) acceptance display, " "(c) circular nodes, (h) horizontal layout, (v) vertical layout, " "(n) with name, (N) without name, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, - { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " + "(i) use implicit labels for complete deterministic automata, " "(s) prefer state-based acceptance when possible [default], " "(t) force transition-based acceptance, " "(m) mix state and transition-based acceptance, " diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 4081980ec..8adbbebb2 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -49,15 +49,18 @@ namespace spot bool has_state_acc; bool is_complete; bool is_deterministic; + bool use_implicit_labels; + bdd all_ap; // Label support: the set of all conditions occurring in the // automaton. typedef std::map sup_map; sup_map sup; - metadata(const const_tgba_digraph_ptr& aut) + metadata(const const_tgba_digraph_ptr& aut, bool implicit) { check_det_and_comp(aut); + use_implicit_labels = implicit && is_deterministic && is_complete; number_all_ap(); } @@ -144,6 +147,7 @@ namespace spot bdd all = bddtrue; for (auto& i: sup) all &= bdd_support(i.first); + all_ap = all; while (all != bddtrue) { @@ -153,6 +157,9 @@ namespace spot vap.push_back(v); } + if (use_implicit_labels) + return; + for (auto& i: sup) { bdd cond = i.first; @@ -199,12 +206,10 @@ namespace spot i.second = s.str(); } } - }; } - enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond }; enum hoa_acceptance { Hoa_Acceptance_States, /// state-based acceptance if @@ -218,17 +223,40 @@ namespace spot static std::ostream& hoa_reachable(std::ostream& os, const const_tgba_digraph_ptr& aut, - hoa_acceptance acceptance, - hoa_alias alias, - bool newline) + const char* opt) { - (void) alias; + bool newline = true; + hoa_acceptance acceptance = Hoa_Acceptance_States; + bool implicit_labels = false; + + if (opt) + while (*opt) + { + switch (*opt++) + { + case 'i': + implicit_labels = true; + break; + case 'l': + newline = false; + break; + case 'm': + acceptance = Hoa_Acceptance_Mixed; + break; + case 's': + acceptance = Hoa_Acceptance_States; + break; + case 't': + acceptance = Hoa_Acceptance_Transitions; + break; + } + } // Calling get_init_state_number() may add a state to empty // automata, so it has to be done first. unsigned init = aut->get_init_state_number(); - metadata md(aut); + metadata md(aut, implicit_labels); if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) acceptance = Hoa_Acceptance_Transitions; @@ -240,9 +268,10 @@ namespace spot auto n = aut->get_named_prop("automaton-name"); if (n) escape_str(os << "name: \"", *n) << '"' << nl; + unsigned nap = md.vap.size(); os << "States: " << num_states << nl << "Start: " << init << nl - << "AP: " << md.vap.size(); + << "AP: " << nap; auto d = aut->get_dict(); for (auto& i: md.vap) { @@ -251,6 +280,7 @@ namespace spot escape_str(os << " \"", f->name()) << '"'; } os << nl; + unsigned num_acc = aut->acc().num_sets(); if (aut->acc().is_generalized_buchi()) { @@ -265,7 +295,12 @@ namespace spot os << "Acceptance: " << num_acc << ' '; os << aut->acc().get_acceptance(); os << nl; - os << "properties: trans-labels explicit-labels"; + os << "properties:"; + implicit_labels = md.use_implicit_labels; + if (implicit_labels) + os << " implicit-labels"; + else + os << " trans-labels explicit-labels"; if (acceptance == Hoa_Acceptance_States) os << " state-acc"; else if (acceptance == Hoa_Acceptance_Transitions) @@ -275,6 +310,18 @@ namespace spot if (md.is_deterministic) os << " deterministic"; os << nl; + + // If we want to output implicit labels, we have to + // fill a vector with all destinations in order. + std::vector out; + std::vector outm; + if (implicit_labels) + { + out.resize(1UL << nap); + if (acceptance != Hoa_Acceptance_States) + outm.resize(1UL << nap); + } + os << "--BODY--" << nl; auto sn = aut->get_named_prop>("state-names"); for (unsigned i = 0; i < num_states; ++i) @@ -299,12 +346,61 @@ namespace spot } os << nl; - for (auto& t: aut->out(i)) + if (!implicit_labels) { - os << '[' << md.sup[t.cond] << "] " << t.dst; - if (this_acc == Hoa_Acceptance_Transitions) - md.emit_acc(os, aut, t.acc); - os << nl; + for (auto& t: aut->out(i)) + { + os << '[' << md.sup[t.cond] << "] " << t.dst; + if (this_acc == Hoa_Acceptance_Transitions) + md.emit_acc(os, aut, t.acc); + os << nl; + } + } + else + { + for (auto& t: aut->out(i)) + { + bdd cond = t.cond; + while (cond != bddfalse) + { + bdd one = bdd_satoneset(cond, md.all_ap, bddfalse); + cond -= one; + unsigned level = 1; + unsigned pos = 0U; + while (one != bddtrue) + { + bdd h = bdd_high(one); + if (h == bddfalse) + { + one = bdd_low(one); + } + else + { + pos |= level; + one = h; + } + level <<= 1; + } + out[pos] = t.dst; + if (this_acc != Hoa_Acceptance_States) + outm[pos] = t.acc; + } + } + unsigned n = out.size(); + for (unsigned i = 0; i < n;) + { + os << out[i]; + if (this_acc != Hoa_Acceptance_States) + { + md.emit_acc(os, aut, outm[i]) << nl; + ++i; + } + else + { + ++i; + os << (((i & 15) && i < n) ? ' ' : nl); + } + } } } os << "--END--"; // No newline. Let the caller decide. @@ -316,35 +412,12 @@ namespace spot const const_tgba_ptr& aut, const char* opt) { - bool newline = true; - hoa_acceptance acceptance = Hoa_Acceptance_States; - hoa_alias alias = Hoa_Alias_None; - - if (opt) - while (*opt) - { - switch (*opt++) - { - case 'l': - newline = false; - break; - case 'm': - acceptance = Hoa_Acceptance_Mixed; - break; - case 's': - acceptance = Hoa_Acceptance_States; - break; - case 't': - acceptance = Hoa_Acceptance_Transitions; - break; - } - } auto a = std::dynamic_pointer_cast(aut); if (!a) a = make_tgba_digraph(aut, tgba::prop_set::all()); - return hoa_reachable(os, a, acceptance, alias, newline); + return hoa_reachable(os, a, opt); } } diff --git a/src/tgbaalgos/hoa.hh b/src/tgbaalgos/hoa.hh index faa7aa5cb..51856fbe0 100644 --- a/src/tgbaalgos/hoa.hh +++ b/src/tgbaalgos/hoa.hh @@ -32,8 +32,10 @@ namespace spot /// \param os The output stream to print on. /// \param g The automaton to output. /// \param opt a set of characters each corresponding to a possible - /// option: (s) state-based acceptance, (t) transition-based - /// acceptance, (m) mixed acceptance, (l) single-line output. + /// option: (i) implicit labels for complete and + /// deterministic automata, (s) state-based acceptance, (t) + /// transition-based acceptance, (m) mixed acceptance, (l) + /// single-line output. SPOT_API std::ostream& hoa_reachable(std::ostream& os, const const_tgba_ptr& g, diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 39dba36d7..d0bd723c3 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -1439,3 +1439,101 @@ State: 0 [!0&!1&!2] 0 {3} --END-- EOF + + +# Implicit labels + +../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' > out.hoa +../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' > out-i.hoa +../../bin/autfilt -C -Hi out.hoa --name=%M > out-i2.hoa +diff out-i.hoa out-i2.hoa + +cat >expected <