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

hierarchy: Rewrite is_recurrence(), is_persistence() and add tests

Browse source 
* spot/tl/hierarchy.cc: Rewrite is_recurrence(), is_persistence()
* spot/tl/hierarchy.hh: Fix typo.
* tests/core/hierarchy.test: Add tests.
This commit is contained in:
Alexandre GBAGUIDI AISSE 2017-11-21 01:20:05 +01:00
parent d89579321f
commit 7e0fc448c5
3 changed files with 86 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

81
spot/tl/hierarchy.cc
View file

@ -81,51 +81,50 @@ namespace spot
}
}
[[noreturn]] static void invalid_spot_pr_check()
{
throw std::runtime_error("invalid value for SPOT_PR_CHECK "
"(should be 1 or 2)");
}
static prcheck
algo_to_perform(bool is_persistence, bool aut_given, prcheck algo)
algo_to_perform(bool is_persistence, bool aut_given)
{
if (algo == prcheck::PR_Auto)
{
// Check environment variable.
static int val_s = []()
static prcheck env_algo = [&]()
{
int val;
try
{
auto s = getenv("SPOT_PR_CHECK");
return s ? std::stoi(s) : 0;
val = s ? std::stoi(s) : 0;
}
catch (const std::exception& e)
{
throw std::runtime_error("invalid value for SPOT_PR_CHECK "
"(should be 1 or 2)");
invalid_spot_pr_check();
}
}();
if (val_s == 1)
{
return prcheck::PR_via_CoBuchi;
}
else if (val_s == 2)
{
return prcheck::PR_via_Rabin;
}
else if (!val_s)
if (val == 0)
{
if (aut_given && !is_persistence)
return prcheck::PR_via_Rabin;
return prcheck::via_Rabin;
else if ((aut_given && is_persistence) || !aut_given)
return prcheck::PR_via_CoBuchi;
return prcheck::via_CoBuchi;
else
SPOT_UNREACHABLE();
}
else if (val == 1)
{
return prcheck::via_CoBuchi;
}
else if (val == 2)
{
return prcheck::via_Rabin;
}
else
{
throw std::runtime_error("invalid value for SPOT_PR_CHECK "
"(should be 1 or 2)");
invalid_spot_pr_check();
}
}
else
return algo;
}();
return env_algo;
}
bool
@ -134,17 +133,20 @@ namespace spot
if (f.is_syntactic_persistence())
return true;
switch (algo_to_perform(true, aut != nullptr, algo))
if (algo == prcheck::Auto)
algo = algo_to_perform(true, aut != nullptr);
switch (algo)
{
case prcheck::PR_via_CoBuchi:
case prcheck::via_CoBuchi:
return cobuchi_realizable(f, aut ? aut :
ltl_to_tgba_fm(f, make_bdd_dict(), true));
case prcheck::PR_via_Rabin:
case prcheck::via_Rabin:
return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f),
make_bdd_dict(), true));
case prcheck::PR_Auto:
case prcheck::Auto:
SPOT_UNREACHABLE();
}
@ -157,18 +159,21 @@ namespace spot
if (f.is_syntactic_recurrence())
return true;
switch (algo_to_perform(false, aut != nullptr, algo))
if (algo == prcheck::Auto)
algo = algo_to_perform(true, aut != nullptr);
switch (algo)
{
case prcheck::PR_via_CoBuchi:
case prcheck::via_CoBuchi:
return cobuchi_realizable(formula::Not(f),
ltl_to_tgba_fm(formula::Not(f),
make_bdd_dict(), true));
case prcheck::PR_via_Rabin:
case prcheck::via_Rabin:
return detbuchi_realizable(aut ? aut :
ltl_to_tgba_fm(f, make_bdd_dict(), true));
case prcheck::PR_Auto:
case prcheck::Auto:
SPOT_UNREACHABLE();
}
@ -221,11 +226,11 @@ namespace spot
case ocheck::via_WDBA:
return is_wdba_realizable(f, aut);
case ocheck::via_CoBuchi:
return (is_persistence(f, aut, prcheck::PR_via_CoBuchi)
&& is_recurrence(f, aut, prcheck::PR_via_CoBuchi));
return (is_persistence(f, aut, prcheck::via_CoBuchi)
&& is_recurrence(f, aut, prcheck::via_CoBuchi));
case ocheck::via_Rabin:
return (is_persistence(f, aut, prcheck::PR_via_Rabin)
&& is_recurrence(f, aut, prcheck::PR_via_Rabin));
return (is_persistence(f, aut, prcheck::via_Rabin)
&& is_recurrence(f, aut, prcheck::via_Rabin));
case ocheck::Auto:
SPOT_UNREACHABLE();
}

10
spot/tl/hierarchy.hh
View file

@ -42,9 +42,9 @@ namespace spot
/// if !f is cobuchi_realizable.
enum class prcheck
{
PR_Auto, // FIXME: Remove the useless PR_ prefix since
PR_via_CoBuchi, // we already have a prcheck:: prefix.
PR_via_Rabin,
Auto,
via_CoBuchi,
via_Rabin,
};
/// \brief Return true if \a f represents a persistence property.
@ -55,7 +55,7 @@ namespace spot
SPOT_API bool
is_persistence(formula f,
twa_graph_ptr aut = nullptr,
prcheck algo = prcheck::PR_Auto);
prcheck algo = prcheck::Auto);
/// \brief Return true if \a f represents a recurrence property.
///
@ -67,7 +67,7 @@ namespace spot
SPOT_API bool
is_recurrence(formula f,
twa_graph_ptr aut = nullptr,
prcheck algo = prcheck::PR_Auto);
prcheck algo = prcheck::Auto);
/// Enum used to change the behavior of is_obligation().
enum class ocheck

34
tests/core/hierarchy.test
View file

@ -66,3 +66,37 @@ diff out expected
test B = `ltlfilt --format=%h -f '(Gb R (b xor Gb)) W (a W Xa)'`
ltlfilt -q --safety --guarantee -f '(Gb R (b xor Gb)) W (a W Xa)'
# make sure SPOT_PR_CHECK is read.
randltl -n -1 a b c | ltlfilt -v --syntactic-safety --syntactic-guarantee \
--syntactic-obligation --syntactic-recurrence --syntactic-persistence \
-n 100 > res
cat res | SPOT_PR_CHECK=x ltlfilt --recurrence 2>err && exit 1
cat res | SPOT_PR_CHECK=9 ltlfilt --recurrence 2>err && exit 1
grep SPOT_PR_CHECK err
# Testing Recurrence.
cat res | ltlfilt --recurrence > r0
for i in 1 2; do
cat res | SPOT_PR_CHECK=$i ltlfilt --recurrence > r$i
done
diff r0 r2
diff r1 r2
cat res | ltlfilt -o %h.ltl
cat R.ltl O.ltl G.ltl S.ltl B.ltl | sort > rogsb.ltl
sort r2 > r3
diff r3 rogsb.ltl
# Testing Persistence.
cat res | ltlfilt --persistence > p0
for i in 1 2; do
cat res | SPOT_PR_CHECK=$i ltlfilt --persistence > p$i
done
diff p0 p2
diff p1 p2
cat res | ltlfilt -o %h.ltl
cat P.ltl O.ltl G.ltl S.ltl B.ltl | sort > pogsb.ltl
sort p2 > p3
diff p3 pogsb.ltl
exit 0