Commit 540b9713 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

gen: rename genltl() to ltl_pattern() and introduce ltl_patterns()

* spot/gen/formulas.hh, spot/gen/formulas.cc (genltl): Rename as...
(ltl_pattern): This.
(ltl_pattern_max): New function.
* bin/genltl.cc: Adjust names, and simplify using ltl_pattern_max().
* python/spot/gen.i (ltl_patterns): New function.
* tests/python/gen.py: Test it.
* tests/python/gen.ipynb: New file to document the spot.gen package.
* tests/Makefile.am, doc/org/tut.org: Add gen.ipynb.
parent 2dc115fe
......@@ -48,7 +48,7 @@ using namespace spot;
const char argp_program_doc[] ="\
Generate temporal logic formulas from predefined patterns.";
// We reuse the values from spot::gen::ltl_patterns as option keys.
// We reuse the values from spot::gen::ltl_pattern_id as option keys.
// Additional options should therefore start after
// spot::gen::LAST_CLASS.
enum {
......@@ -171,7 +171,7 @@ static const argp_option options[] =
struct job
{
spot::gen::ltl_pattern pattern;
spot::gen::ltl_pattern_id pattern;
struct range range;
};
......@@ -188,54 +188,36 @@ const struct argp_child children[] =
};
static void
enqueue_job(int pattern, const char* range_str)
enqueue_job(int pattern, const char* range_str = nullptr)
{
job j;
j.pattern = static_cast<spot::gen::ltl_pattern>(pattern);
j.range = parse_range(range_str);
jobs.push_back(j);
}
static void
enqueue_job(int pattern, int min, int max)
{
job j;
j.pattern = static_cast<spot::gen::ltl_pattern>(pattern);
j.range = {min, max};
j.pattern = static_cast<spot::gen::ltl_pattern_id>(pattern);
if (range_str)
{
j.range = parse_range(range_str);
}
else
{
j.range.min = 1;
j.range.max = spot::gen::ltl_pattern_max(j.pattern);
if (j.range.max == 0)
error(2, 0, "missing range for %s",
spot::gen::ltl_pattern_name(j.pattern));
}
jobs.push_back(j);
}
static int
parse_opt(int key, char* arg, struct argp_state*)
{
if (key >= spot::gen::FIRST_CLASS && key < spot::gen::LAST_CLASS)
{
enqueue_job(key, arg);
return 0;
}
// This switch is alphabetically-ordered.
switch (key)
{
case spot::gen::DAC_PATTERNS:
case spot::gen::HKRSS_PATTERNS:
if (arg)
enqueue_job(key, arg);
else
enqueue_job(key, 1, 55);
break;
case spot::gen::EH_PATTERNS:
if (arg)
enqueue_job(key, arg);
else
enqueue_job(key, 1, 12);
break;
case spot::gen::P_PATTERNS:
if (arg)
enqueue_job(key, arg);
else
enqueue_job(key, 1, 20);
break;
case spot::gen::SB_PATTERNS:
if (arg)
enqueue_job(key, arg);
else
enqueue_job(key, 1, 27);
break;
case OPT_POSITIVE:
opt_positive = true;
break;
......@@ -243,11 +225,6 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_negative = true;
break;
default:
if (key >= spot::gen::FIRST_CLASS && key < spot::gen::LAST_CLASS)
{
enqueue_job(key, arg);
break;
}
return ARGP_ERR_UNKNOWN;
}
return 0;
......@@ -255,9 +232,9 @@ parse_opt(int key, char* arg, struct argp_state*)
static void
output_pattern(spot::gen::ltl_pattern pattern, int n)
output_pattern(spot::gen::ltl_pattern_id pattern, int n)
{
formula f = spot::gen::genltl(pattern, n);
formula f = spot::gen::ltl_pattern(pattern, n);
// Make sure we use only "p42"-style of atomic propositions
// in lbt's output.
......
......@@ -69,6 +69,7 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
in Python
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
- [[https://spot.lrde.epita.fr/ipynb/gen.html][=gen.ipynb=]] show how to generate families of LTL formulas (as done in [[file:genltl.org][=genltl=]]) or automata ([[file:genaut.org][=genaut=]])
- [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()=, =decompose_acc_scc()= and =decompose_scc()= functions
- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing
automaton
......
......@@ -53,3 +53,36 @@ using namespace spot;
%include <spot/gen/automata.hh>
%include <spot/gen/formulas.hh>
%pythoncode %{
def ltl_patterns(*args):
"""
Generate LTL patterns.
The arguments should be have one of these three forms:
- (id, n)
- (id, min, max)
- id
In the first case, the pattern id=n is generated. In the second
case, all pattern id=n for min<=n<=max are generated. The
third case is a shorthand for (id, 1, 10), except when
id denotes one of the hard-coded list of LTL formulas (like,
DAC_PATTERNS, EH_PATTERNS, etc.) where all formulas from that
list are output.
"""
for spec in args:
if type(spec) is int:
pat = spec
min = 1
max = ltl_pattern_max(spec) or 10
else:
ls = len(spec)
if ls == 2:
pat, min, max = spec[0], spec[1], spec[1]
elif ls == 3:
pat, min, max = spec
else:
raise RuntimeError("invalid pattern specification")
for n in range(min, max + 1):
yield ltl_pattern(pat, n)
%}
......@@ -1041,7 +1041,7 @@ namespace spot
}
}
formula genltl(ltl_pattern pattern, int n)
formula ltl_pattern(ltl_pattern_id pattern, int n)
{
if (n < 0)
{
......@@ -1127,7 +1127,7 @@ namespace spot
}
const char* ltl_pattern_name(ltl_pattern pattern)
const char* ltl_pattern_name(ltl_pattern_id pattern)
{
static const char* const class_name[] =
{
......@@ -1174,6 +1174,60 @@ namespace spot
return class_name[pattern - FIRST_CLASS];
}
int ltl_pattern_max(ltl_pattern_id pattern)
{
switch (pattern)
{
// Keep this alphabetically-ordered!
case AND_F:
case AND_FG:
case AND_GF:
case CCJ_ALPHA:
case CCJ_BETA:
case CCJ_BETA_PRIME:
return 0;
case DAC_PATTERNS:
return 55;
case EH_PATTERNS:
return 12;
case GH_Q:
case GH_R:
case GO_THETA:
return 0;
case HKRSS_PATTERNS:
return 55;
case KR_N:
case KR_NLOGN:
case KV_PSI:
case OR_FG:
case OR_G:
case OR_GF:
return 0;
case P_PATTERNS:
return 20;
case R_LEFT:
case R_RIGHT:
case RV_COUNTER_CARRY:
case RV_COUNTER_CARRY_LINEAR:
case RV_COUNTER:
case RV_COUNTER_LINEAR:
return 0;
case SB_PATTERNS:
return 27;
case TV_F1:
case TV_F2:
case TV_G1:
case TV_G2:
case TV_UU:
case U_LEFT:
case U_RIGHT:
return 0;
case LAST_CLASS:
break;
}
throw std::runtime_error("unsupported pattern");
}
}
}
......@@ -165,7 +165,7 @@ namespace spot
{
namespace gen
{
enum ltl_pattern {
enum ltl_pattern_id {
FIRST_CLASS = 256,
AND_F = FIRST_CLASS,
AND_FG,
......@@ -205,15 +205,21 @@ namespace spot
/// \brief generate an LTL from a known pattern
///
/// The pattern is specified using one value from the ltl_pattern
/// The pattern is specified using one value from the ltl_pattern_id
/// enum. See the man page of the `genltl` binary for a
/// description of those pattern, and bibliographic references.
SPOT_API formula genltl(ltl_pattern pattern, int n);
SPOT_API formula ltl_pattern(ltl_pattern_id pattern, int n);
/// \brief convert an ltl_pattern value into a name
///
/// The returned name is suitable to be used as an option
/// key for the genltl binary.
SPOT_API const char* ltl_pattern_name(ltl_pattern pattern);
SPOT_API const char* ltl_pattern_name(ltl_pattern_id pattern);
/// \brief upper bound for LTL patterns
///
/// If an LTL pattern has an upper bound, this returns it.
/// Otherwise, this returns 0.
SPOT_API int ltl_pattern_max(ltl_pattern_id pattern);
}
}
......@@ -310,6 +310,7 @@ TESTS_ipython = \
python/automata.ipynb \
python/decompose.ipynb \
python/formulas.ipynb \
python/gen.ipynb \
python/highlighting.ipynb \
python/ltsmin-dve.ipynb \
python/ltsmin-pml.ipynb \
......
This diff is collapsed.
......@@ -38,21 +38,25 @@ except RuntimeError as e:
else:
exit(2)
f = gen.genltl(gen.AND_F, 3)
f = gen.ltl_pattern(gen.AND_F, 3)
assert f.size() == 3
assert gen.ltl_pattern_name(gen.AND_F) == "and-f"
try:
gen.genltl(1000, 3)
gen.ltl_pattern(1000, 3)
except RuntimeError as e:
assert 'unsupported pattern' in str(e)
else:
exit(2)
try:
gen.genltl(gen.OR_G, -10)
gen.ltl_pattern(gen.OR_G, -10)
except RuntimeError as e:
assert 'or-g' in str(e)
assert 'positive' in str(e)
else:
exit(2)
assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.OR_G, 1, 5),
(gen.GH_Q, 3),
gen.EH_PATTERNS))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment