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

acc: add a maybe_accepting() method

Browse source 
* spot/twa/acc.cc, spot/twa/acc.hh: Implement the new method, and
use it to implement inf_accepting().
* tests/python/accparse2.py: Add some tests.
This commit is contained in:
Alexandre Duret-Lutz 2017-05-30 18:04:57 +02:00
parent f7d14ab526
commit 78add1d44b
3 changed files with 54 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

45
spot/twa/acc.cc
View file

@ -215,39 +215,52 @@ namespace spot
return false;
}
static bool
inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
static trival
partial_eval(acc_cond::mark_t infinitely_often,
acc_cond::mark_t always_present,
const acc_cond::acc_word* pos)
{
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
{
auto sub = pos - pos->sub.size;
trival res = true;
while (sub < pos)
{
--pos;
if (!inf_eval(inf, pos))
return false;
res = res &&
partial_eval(infinitely_often, always_present, pos);
if (res.is_false())
return res;
pos -= pos->sub.size;
}
return true;
return res;
}
case acc_cond::acc_op::Or:
{
auto sub = pos - pos->sub.size;
trival res = false;
while (sub < pos)
{
--pos;
if (inf_eval(inf, pos))
return true;
res = res ||
partial_eval(infinitely_often, always_present, pos);
if (res.is_true())
return res;
pos -= pos->sub.size;
}
return false;
return res;
}
case acc_cond::acc_op::Inf:
return (pos[-1].mark & inf) == pos[-1].mark;
return (pos[-1].mark & infinitely_often) == pos[-1].mark;
case acc_cond::acc_op::Fin:
return true;
if (pos[-1].mark & always_present)
return false;
else if (pos[-1].mark & infinitely_often)
return trival::maybe();
else
return true;
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
@ -310,13 +323,21 @@ namespace spot
return eval(inf, &back());
}
bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const
trival acc_cond::acc_code::maybe_accepting(mark_t infinitely_often,
mark_t always_present) const
{
if (empty())
return true;
return inf_eval(inf, &back());
return partial_eval(infinitely_often | always_present,
always_present, &back());
}
bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const
{
return !maybe_accepting(inf, 0U).is_false();
}
acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const
{
if (uses_fin_acceptance())

10
spot/twa/acc.hh
View file

@ -24,6 +24,7 @@
#include <sstream>
#include <vector>
#include <spot/tl/defaultenv.hh>
#include <spot/misc/trival.hh>
#include <iostream>
namespace spot
@ -888,6 +889,10 @@ namespace spot
bool inf_satisfiable(mark_t inf) const;
trival maybe_accepting(mark_t infinitely_often,
mark_t always_present) const;
// Remove all the acceptance sets in rem.
//
// If MISSING is set, the acceptance sets are assumed to be
@ -1238,6 +1243,11 @@ namespace spot
return code_.inf_satisfiable(inf);
}
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
{
return code_.maybe_accepting(infinitely_often, always_present);
}
mark_t accepting_sets(mark_t inf) const;
std::ostream& format(std::ostream& os, mark_t m) const

12
tests/python/accparse2.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@ -31,6 +31,16 @@ a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')
assert(a.is_parity()[0] == False)
assert(a.is_parity(True) == [True, True, False])
assert a.maybe_accepting([1, 2, 3], [0, 4]).is_true()
assert a.maybe_accepting([0], []).is_true()
assert a.maybe_accepting([0], [3]).is_false()
assert a.maybe_accepting([0, 3], []).is_maybe()
assert a.maybe_accepting([2, 3], [3]).is_false()
assert a.maybe_accepting([2, 3], []).is_maybe()
assert a.maybe_accepting([2], []).is_true()
assert a.maybe_accepting([0, 1], []).is_maybe()
assert a.maybe_accepting([0, 1], [1]).is_false()
a = spot.acc_cond(0)
a.set_acceptance('all')
assert(a.is_rabin() == -1)