acc: introduce acc_cond::name()
* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::name): New method. * spot/twaalgos/dot.cc: Use it. * tests/python/acc_cond.ipynb: Add a small test. * NEWS: Mention it.
This commit is contained in:
parent
4711dcd74f
commit
bd39edde27
5 changed files with 215 additions and 86 deletions
4
NEWS
4
NEWS
|
|
@ -140,6 +140,10 @@ New in spot 2.4.1.dev (not yet released)
|
||||||
optimization for stutter-invariant automata that may produce slightly
|
optimization for stutter-invariant automata that may produce slightly
|
||||||
smaller automata.
|
smaller automata.
|
||||||
|
|
||||||
|
- acc_cond::name(fmt) is a new method that name well-known acceptance
|
||||||
|
conditions. The fmt parameter specify the format to use for that
|
||||||
|
name (e.g. to the style used in HOA, or that used by print_dot()).
|
||||||
|
|
||||||
Deprecation notices:
|
Deprecation notices:
|
||||||
|
|
||||||
(These functions still work but compilers emit warnings.)
|
(These functions still work but compilers emit warnings.)
|
||||||
|
|
|
||||||
158
spot/twa/acc.cc
158
spot/twa/acc.cc
|
|
@ -1498,6 +1498,164 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/// Return the name of this acceptance condition, in the
|
||||||
|
/// specified format.
|
||||||
|
std::string acc_cond::name(const char* fmt) const
|
||||||
|
{
|
||||||
|
bool accentuated = false;
|
||||||
|
bool no_extra_param = false;
|
||||||
|
bool no_main_param = false;
|
||||||
|
bool no_parity_param = false;
|
||||||
|
bool abbreviate = false;
|
||||||
|
bool like_names = false;
|
||||||
|
bool other = false;
|
||||||
|
|
||||||
|
if (fmt)
|
||||||
|
while (*fmt)
|
||||||
|
switch (char c = *fmt++)
|
||||||
|
{
|
||||||
|
case '0': // no param style
|
||||||
|
no_extra_param = no_main_param = no_parity_param = true;
|
||||||
|
break;
|
||||||
|
case 'a':
|
||||||
|
accentuated = true;
|
||||||
|
break;
|
||||||
|
case 'b':
|
||||||
|
abbreviate = true;
|
||||||
|
break;
|
||||||
|
case 'd': // print_dot() style
|
||||||
|
accentuated = no_extra_param = abbreviate = like_names = true;
|
||||||
|
break;
|
||||||
|
case 'g':
|
||||||
|
no_extra_param = true;
|
||||||
|
break;
|
||||||
|
case 'l':
|
||||||
|
like_names = true;
|
||||||
|
break;
|
||||||
|
case 'm':
|
||||||
|
no_main_param = true;
|
||||||
|
break;
|
||||||
|
case 'p':
|
||||||
|
no_parity_param = true;
|
||||||
|
break;
|
||||||
|
case 'o':
|
||||||
|
other = true;
|
||||||
|
break;
|
||||||
|
case 's':
|
||||||
|
other = no_extra_param = no_main_param = no_parity_param =
|
||||||
|
like_names = true;
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
throw std::runtime_error
|
||||||
|
(std::string("unknown option for acc_cond::name(): ") + c);
|
||||||
|
}
|
||||||
|
|
||||||
|
std::ostringstream os;
|
||||||
|
|
||||||
|
auto gen = [abbreviate]()
|
||||||
|
{
|
||||||
|
return abbreviate ? "gen. " : "generalized-";
|
||||||
|
};
|
||||||
|
auto sets = [no_main_param, this]() -> std::string
|
||||||
|
{
|
||||||
|
return no_main_param ? "" : " " + std::to_string(num_sets());
|
||||||
|
};
|
||||||
|
|
||||||
|
if (is_generalized_buchi())
|
||||||
|
{
|
||||||
|
if (is_all())
|
||||||
|
os << "all";
|
||||||
|
else if (is_buchi())
|
||||||
|
os << (accentuated ? "Büchi" : "Buchi");
|
||||||
|
else
|
||||||
|
os << gen() << (accentuated ? "Büchi" : "Buchi") << sets();
|
||||||
|
}
|
||||||
|
else if (is_generalized_co_buchi())
|
||||||
|
{
|
||||||
|
if (is_none())
|
||||||
|
os << "none";
|
||||||
|
else if (is_co_buchi())
|
||||||
|
os << (accentuated ? "co-Büchi" : "co-Buchi");
|
||||||
|
else
|
||||||
|
os << gen() << (accentuated ? "co-Büchi" : "co-Buchi") << sets();
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
int r = is_rabin();
|
||||||
|
assert(r != 0);
|
||||||
|
if (r > 0)
|
||||||
|
{
|
||||||
|
os << "Rabin";
|
||||||
|
if (!no_main_param)
|
||||||
|
os << ' ' << r;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
r = is_streett();
|
||||||
|
assert(r != 0);
|
||||||
|
if (r > 0)
|
||||||
|
{
|
||||||
|
os << "Streett";
|
||||||
|
if (!no_main_param)
|
||||||
|
os << ' ' << r;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
std::vector<unsigned> pairs;
|
||||||
|
if (is_generalized_rabin(pairs))
|
||||||
|
{
|
||||||
|
os << gen() << "Rabin";
|
||||||
|
if (!no_main_param)
|
||||||
|
{
|
||||||
|
os << ' ' << pairs.size();
|
||||||
|
if (!no_extra_param)
|
||||||
|
for (auto p: pairs)
|
||||||
|
os << ' ' << p;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
bool max = false;
|
||||||
|
bool odd = false;
|
||||||
|
if (is_parity(max, odd))
|
||||||
|
{
|
||||||
|
os << "parity";
|
||||||
|
if (!no_parity_param)
|
||||||
|
os << (max ? " max" : " min")
|
||||||
|
<< (odd ? " odd" : " even");
|
||||||
|
os << sets();
|
||||||
|
}
|
||||||
|
else if (like_names)
|
||||||
|
{
|
||||||
|
std::vector<acc_cond::rs_pair> r_pairs;
|
||||||
|
bool r_like = is_rabin_like(r_pairs);
|
||||||
|
unsigned rsz = r_pairs.size();
|
||||||
|
std::vector<acc_cond::rs_pair> s_pairs;
|
||||||
|
bool s_like = is_streett_like(s_pairs);
|
||||||
|
unsigned ssz = s_pairs.size();
|
||||||
|
if (r_like && (!s_like || (rsz <= ssz)))
|
||||||
|
{
|
||||||
|
os << "Rabin-like";
|
||||||
|
if (!no_main_param)
|
||||||
|
os << ' ' << rsz;
|
||||||
|
}
|
||||||
|
else if (s_like && (!r_like || (ssz < rsz)))
|
||||||
|
{
|
||||||
|
os << "Streett-like";
|
||||||
|
if (!no_main_param)
|
||||||
|
os << ' ' << ssz;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
std::string res = os.str();
|
||||||
|
if (other && res.empty())
|
||||||
|
res = "other" + sets();
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -33,6 +33,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
class mark_container;
|
class mark_container;
|
||||||
}
|
}
|
||||||
|
|
||||||
class SPOT_API acc_cond
|
class SPOT_API acc_cond
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
@ -899,7 +900,6 @@ namespace spot
|
||||||
std::function<void(std::ostream&, int)>
|
std::function<void(std::ostream&, int)>
|
||||||
set_printer = nullptr) const;
|
set_printer = nullptr) const;
|
||||||
|
|
||||||
|
|
||||||
/// \brief Construct an acc_code from a string.
|
/// \brief Construct an acc_code from a string.
|
||||||
///
|
///
|
||||||
/// The string can follow the following grammar:
|
/// The string can follow the following grammar:
|
||||||
|
|
@ -1313,6 +1313,19 @@ namespace spot
|
||||||
return {num_sets(), code_.remove(all_sets() - rem, true)};
|
return {num_sets(), code_.remove(all_sets() - rem, true)};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// \brief Return the name of this acceptance condition, in the
|
||||||
|
/// specified format.
|
||||||
|
///
|
||||||
|
/// The empty string is returned if no name is known.
|
||||||
|
///
|
||||||
|
/// \a fmt should be a combination of the following letters. (0)
|
||||||
|
/// no parameters, (a) accentuated, (b) abbreviated, (d) style
|
||||||
|
/// used in dot output, (g) no generalized parameter, (l)
|
||||||
|
/// recognize Street-like and Rabin-like, (m) no main parameter,
|
||||||
|
/// (p) no parity parameter, (o) name unknown acceptance as
|
||||||
|
/// 'other', (s) shorthand for 'lo0'.
|
||||||
|
std::string name(const char* fmt = "alo") const;
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
mark_t::value_t all_sets_() const
|
mark_t::value_t all_sets_() const
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -455,85 +455,9 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
std::string get_acceptance_for_human()
|
|
||||||
{
|
|
||||||
std::ostringstream os;
|
|
||||||
|
|
||||||
if (aut_->acc().is_generalized_buchi())
|
|
||||||
{
|
|
||||||
if (aut_->acc().is_all())
|
|
||||||
os << "all";
|
|
||||||
else if (aut_->acc().is_buchi())
|
|
||||||
os << "Büchi";
|
|
||||||
else
|
|
||||||
os << "gen. Büchi " << aut_->num_sets();
|
|
||||||
}
|
|
||||||
else if (aut_->acc().is_generalized_co_buchi())
|
|
||||||
{
|
|
||||||
if (aut_->acc().is_none())
|
|
||||||
os << "none";
|
|
||||||
else if (aut_->acc().is_co_buchi())
|
|
||||||
os << "co-Büchi";
|
|
||||||
else
|
|
||||||
os << "gen. co-Büchi " << aut_->num_sets();
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
int r = aut_->acc().is_rabin();
|
|
||||||
assert(r != 0);
|
|
||||||
if (r > 0)
|
|
||||||
{
|
|
||||||
os << "Rabin " << r;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
r = aut_->acc().is_streett();
|
|
||||||
assert(r != 0);
|
|
||||||
if (r > 0)
|
|
||||||
{
|
|
||||||
os << "Streett " << r;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
std::vector<unsigned> pairs;
|
|
||||||
if (aut_->acc().is_generalized_rabin(pairs))
|
|
||||||
{
|
|
||||||
os << "gen. Rabin " << pairs.size();
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
bool max = false;
|
|
||||||
bool odd = false;
|
|
||||||
if (aut_->acc().is_parity(max, odd))
|
|
||||||
{
|
|
||||||
os << "parity "
|
|
||||||
<< (max ? "max " : "min ")
|
|
||||||
<< (odd ? "odd " : "even ")
|
|
||||||
<< aut_->num_sets();
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
std::vector<acc_cond::rs_pair> r_pairs;
|
|
||||||
bool r_like = aut_->acc().is_rabin_like(r_pairs);
|
|
||||||
unsigned rsz = r_pairs.size();
|
|
||||||
std::vector<acc_cond::rs_pair> s_pairs;
|
|
||||||
bool s_like = aut_->acc().is_streett_like(s_pairs);
|
|
||||||
unsigned ssz = s_pairs.size();
|
|
||||||
if (r_like && (!s_like || (rsz <= ssz)))
|
|
||||||
os << "Rabin-like " << rsz;
|
|
||||||
else if (s_like && (!r_like || (ssz < rsz)))
|
|
||||||
os << "Streett-like " << ssz;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return os.str();
|
|
||||||
}
|
|
||||||
|
|
||||||
void print_acceptance_for_human()
|
void print_acceptance_for_human()
|
||||||
{
|
{
|
||||||
std::string accstr = get_acceptance_for_human();
|
std::string accstr = aut_->acc().name("d");
|
||||||
if (accstr.empty())
|
if (accstr.empty())
|
||||||
return;
|
return;
|
||||||
os_ << nl_ << '[' << accstr << ']';
|
os_ << nl_ << '[' << accstr << ']';
|
||||||
|
|
|
||||||
|
|
@ -15,7 +15,7 @@
|
||||||
"name": "python",
|
"name": "python",
|
||||||
"nbconvert_exporter": "python",
|
"nbconvert_exporter": "python",
|
||||||
"pygments_lexer": "ipython3",
|
"pygments_lexer": "ipython3",
|
||||||
"version": "3.5.4"
|
"version": "3.6.3"
|
||||||
},
|
},
|
||||||
"name": ""
|
"name": ""
|
||||||
},
|
},
|
||||||
|
|
@ -1266,6 +1266,36 @@
|
||||||
],
|
],
|
||||||
"prompt_number": 46
|
"prompt_number": 46
|
||||||
},
|
},
|
||||||
|
{
|
||||||
|
"cell_type": "markdown",
|
||||||
|
"metadata": {},
|
||||||
|
"source": [
|
||||||
|
"If the acceptance condition has some known name, it can be retrieved using the `name()` method. By default the name given is a human-readable string close that used in the HOA format, but with proper accents, and support for name like `Streett-like` or `Rabin-like`. The argument `arg` can specify a different style using the same syntax as in `--format='%[arg]g'` when using the command-line tools."
|
||||||
|
]
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"cell_type": "code",
|
||||||
|
"collapsed": false,
|
||||||
|
"input": [
|
||||||
|
"print(acc.name())\n",
|
||||||
|
"print(acc.name(\"d\")) # <- Style used by print_dot(aut, \"a\")\n",
|
||||||
|
"print(acc.name(\"0\")) # <- no parameters"
|
||||||
|
],
|
||||||
|
"language": "python",
|
||||||
|
"metadata": {},
|
||||||
|
"outputs": [
|
||||||
|
{
|
||||||
|
"output_type": "stream",
|
||||||
|
"stream": "stdout",
|
||||||
|
"text": [
|
||||||
|
"generalized-B\u00fcchi 4\n",
|
||||||
|
"gen. B\u00fcchi 4\n",
|
||||||
|
"generalized-Buchi\n"
|
||||||
|
]
|
||||||
|
}
|
||||||
|
],
|
||||||
|
"prompt_number": 47
|
||||||
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
|
|
@ -1293,7 +1323,7 @@
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 47
|
"prompt_number": 48
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
|
|
@ -1314,13 +1344,13 @@
|
||||||
{
|
{
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"output_type": "pyout",
|
"output_type": "pyout",
|
||||||
"prompt_number": 48,
|
"prompt_number": 49,
|
||||||
"text": [
|
"text": [
|
||||||
"{0,1,2,3}"
|
"{0,1,2,3}"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 48
|
"prompt_number": 49
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
|
|
@ -1351,7 +1381,7 @@
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 49
|
"prompt_number": 50
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "markdown",
|
"cell_type": "markdown",
|
||||||
|
|
@ -1381,7 +1411,7 @@
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 50
|
"prompt_number": 51
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "code",
|
"cell_type": "code",
|
||||||
|
|
@ -1403,7 +1433,7 @@
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 51
|
"prompt_number": 52
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "code",
|
"cell_type": "code",
|
||||||
|
|
@ -1425,7 +1455,7 @@
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 52
|
"prompt_number": 53
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"metadata": {}
|
"metadata": {}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue