* src/ltltest/genltl.cc (fair_response): Typo.
This commit is contained in:
parent
d47aa1d8b2
commit
bb06db7c1b
2 changed files with 5 additions and 1 deletions
|
|
@ -1,3 +1,7 @@
|
||||||
|
2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
* src/ltltest/genltl.cc (fair_response): Typo.
|
||||||
|
|
||||||
2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2011-06-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
DVE2: Do not display state variables with only one possible value.
|
DVE2: Do not display state variables with only one possible value.
|
||||||
|
|
|
||||||
|
|
@ -411,7 +411,7 @@ formula* combunop_n(std::string name, int n,
|
||||||
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
|
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
|
||||||
formula* fair_response(std::string p, std::string q, std::string r, int n)
|
formula* fair_response(std::string p, std::string q, std::string r, int n)
|
||||||
{
|
{
|
||||||
formula* fair = GF_n("p", n);
|
formula* fair = GF_n(p, n);
|
||||||
formula* resp = G_(Implies_(env.require(q), F_(env.require(r))));
|
formula* resp = G_(Implies_(env.require(q), F_(env.require(r))));
|
||||||
return Not_(Implies_(fair, resp));
|
return Not_(Implies_(fair, resp));
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue