alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

genltl: --ms-example now has two arguments

Browse source 
* bin/genltl.cc, spot/gen/formulas.cc, tests/core/genltl.test: Adjust.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-03 19:35:02 +02:00
parent 2e50f9e986
commit c535871ffd
4 changed files with 62 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -34,6 +34,9 @@ New in spot 2.5.3.dev (not yet released)
--sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] --sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16]
paper (range should be included in 1..3) paper (range should be included in 1..3)
- genltl --ms-example can now take a two-range argument,
(as --sejk-f above).
Library: Library:
- spot::twa_graph::merge_states() is a new method that merges states - spot::twa_graph::merge_states() is a new method that merges states

4
bin/genltl.cc
View file

@ -110,8 +110,8 @@ static const argp_option options[] =
{ "kv-psi", gen::LTL_KV_PSI, "RANGE", 0, { "kv-psi", gen::LTL_KV_PSI, "RANGE", 0,
"quadratic formula with doubly exponential DBA", 0 }, "quadratic formula with doubly exponential DBA", 0 },
OPT_ALIAS(kr-n2), OPT_ALIAS(kr-n2),
{ "ms-example", gen::LTL_MS_EXAMPLE, "RANGE", 0, { "ms-example", gen::LTL_MS_EXAMPLE, "RANGE[,RANGE]", 0,
"GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...)))", 0 }, "GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))", 0 },
{ "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0, { "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0,
"FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...", 0 }, "FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...", 0 },
{ "ms-phi-r", gen::LTL_MS_PHI_R, "RANGE", 0, { "ms-phi-r", gen::LTL_MS_PHI_R, "RANGE", 0,

17
spot/gen/formulas.cc
View file

@ -43,19 +43,14 @@ namespace spot
namespace namespace
{ {
static formula static formula
ms_example(const char* a, const char* b, int n) ms_example(const char* a, const char* b, int n, int m)
{ {
formula ax = formula::tt(); formula ax = formula::tt();
formula fb = formula::tt(); formula fb = formula::tt();
for (int i = n; i > 0; --i) for (int i = n; i > 0; --i)
{ ax = And_(formula::ap(a + std::to_string(i)), X_(ax));
std::ostringstream ans; for (int i = m; i > 0; --i)
ans << a << i; fb = F_(And_(formula::ap(b + std::to_string(i)), fb));
ax = And_(formula::ap(ans.str()), X_(ax));
ans.str("");
ans << b << i;
fb = F_(And_(formula::ap(ans.str()), fb));
}
return And_(G_(F_(ax)), fb); return And_(G_(F_(ax)), fb);
} }
@ -1255,7 +1250,7 @@ namespace spot
case LTL_OR_GF: case LTL_OR_GF:
return GF_n("p", n, false); return GF_n("p", n, false);
case LTL_MS_EXAMPLE: case LTL_MS_EXAMPLE:
return ms_example("a", "b", n); return ms_example("a", "b", n, m);
case LTL_MS_PHI_H: case LTL_MS_PHI_H:
return ms_phi_h("a", "b", n); return ms_phi_h("a", "b", n);
case LTL_MS_PHI_R: case LTL_MS_PHI_R:
@ -1458,7 +1453,9 @@ namespace spot
case LTL_KR_N: case LTL_KR_N:
case LTL_KR_NLOGN: case LTL_KR_NLOGN:
case LTL_KV_PSI: case LTL_KV_PSI:
return 1;
case LTL_MS_EXAMPLE: case LTL_MS_EXAMPLE:
return 2;
case LTL_MS_PHI_H: case LTL_MS_PHI_H:
case LTL_MS_PHI_R: case LTL_MS_PHI_R:
case LTL_MS_PHI_S: case LTL_MS_PHI_S:

80
tests/core/genltl.test
View file

@ -154,43 +154,63 @@ test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16
test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16 test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16
genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \ genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
--gf-equiv=0..5 --gf-implies=0..5 --format=%F=%L,%f | --gf-equiv=0..5 --gf-implies=0..5 --format='"%F=%L",%f' |
ltl2tgba -G -D -F-/2 --stats='%<,%s' > out ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
cat >exp<<EOF cat >exp<<EOF
ms-example=0,1 "ms-example=0,0",1
ms-example=1,2 "ms-example=0,1",2
ms-example=2,4 "ms-example=0,2",3
ms-example=3,7 "ms-example=0,3",4
ms-example=4,12 "ms-example=0,4",5
ms-phi-r=0,2 "ms-example=1,0",1
ms-phi-r=1,16 "ms-example=1,1",2
ms-phi-r=2,29 "ms-example=1,2",3
ms-phi-s=0,5 "ms-example=1,3",4
ms-phi-s=1,8 "ms-example=1,4",5
ms-phi-s=2,497 "ms-example=2,0",2
ms-phi-h=0,1 "ms-example=2,1",3
ms-phi-h=1,3 "ms-example=2,2",4
ms-phi-h=2,7 "ms-example=2,3",5
ms-phi-h=3,15 "ms-example=2,4",6
ms-phi-h=4,31 "ms-example=3,0",4
gf-equiv=0,1 "ms-example=3,1",5
gf-equiv=1,4 "ms-example=3,2",6
gf-equiv=2,8 "ms-example=3,3",7
gf-equiv=3,21 "ms-example=3,4",8
gf-equiv=4,81 "ms-example=4,0",8
gf-equiv=5,431 "ms-example=4,1",9
gf-implies=0,1 "ms-example=4,2",10
gf-implies=1,5 "ms-example=4,3",11
gf-implies=2,12 "ms-example=4,4",12
gf-implies=3,41 "ms-phi-r=0",2
gf-implies=4,186 "ms-phi-r=1",16
gf-implies=5,1047 "ms-phi-r=2",29
"ms-phi-s=0",5
"ms-phi-s=1",8
"ms-phi-s=2",497
"ms-phi-h=0",1
"ms-phi-h=1",3
"ms-phi-h=2",7
"ms-phi-h=3",15
"ms-phi-h=4",31
"gf-equiv=0",1
"gf-equiv=1",4
"gf-equiv=2",8
"gf-equiv=3",21
"gf-equiv=4",81
"gf-equiv=5",431
"gf-implies=0",1
"gf-implies=1",5
"gf-implies=2",12
"gf-implies=3",41
"gf-implies=4",186
"gf-implies=5",1047
EOF EOF
diff out exp diff out exp
# Running ltl2tgba on one formula at a time should give the same results # Running ltl2tgba on one formula at a time should give the same results
genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \ genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
--gf-equiv=0..5 --gf-implies=0..5 --format=%F=%L,%f | --gf-equiv=0..5 --gf-implies=0..5 --format='"%F=%L",%f' |
ltldo -F-/2 'ltl2tgba -G -D' --stats='%<,%s' > out ltldo -F-/2 'ltl2tgba -G -D' --stats='%<,%s' > out
diff out exp diff out exp