simplify: fix some discrepancies between Intel and ARM
* spot/tl/simplify.cc (tl_simplifier_cache::as_bdd): Fix the order in which as_bdd() is called recursively in binary nodes, do not let the choice to the compiler. * tests/core/ltlsynt.test: Adjust expected output.
This commit is contained in:
parent
1b69ed96f9
commit
644342f5d4
2 changed files with 25 additions and 11 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
|
// Copyright (C) 2011-2021 Laboratoire de Recherche et Developpement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -125,14 +125,23 @@ namespace spot
|
||||||
result = !as_bdd(f[0]);
|
result = !as_bdd(f[0]);
|
||||||
break;
|
break;
|
||||||
case op::Xor:
|
case op::Xor:
|
||||||
result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_xor);
|
{
|
||||||
break;
|
bdd l = as_bdd(f[0]);
|
||||||
|
result = bdd_apply(l, as_bdd(f[1]), bddop_xor);
|
||||||
|
break;
|
||||||
|
}
|
||||||
case op::Implies:
|
case op::Implies:
|
||||||
result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_imp);
|
{
|
||||||
break;
|
bdd l = as_bdd(f[0]);
|
||||||
|
result = bdd_apply(l, as_bdd(f[1]), bddop_imp);
|
||||||
|
break;
|
||||||
|
}
|
||||||
case op::Equiv:
|
case op::Equiv:
|
||||||
result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_biimp);
|
{
|
||||||
break;
|
bdd l = as_bdd(f[0]);
|
||||||
|
result = bdd_apply(l, as_bdd(f[1]), bddop_biimp);
|
||||||
|
break;
|
||||||
|
}
|
||||||
case op::And:
|
case op::And:
|
||||||
{
|
{
|
||||||
result = bddtrue;
|
result = bddtrue;
|
||||||
|
|
@ -4038,9 +4047,14 @@ namespace spot
|
||||||
bool result;
|
bool result;
|
||||||
|
|
||||||
if (f.is_boolean() && g.is_boolean())
|
if (f.is_boolean() && g.is_boolean())
|
||||||
result = bdd_implies(as_bdd(f), as_bdd(g));
|
{
|
||||||
|
bdd l = as_bdd(f);
|
||||||
|
result = bdd_implies(l, as_bdd(g));
|
||||||
|
}
|
||||||
else
|
else
|
||||||
result = syntactic_implication_aux(f, g);
|
{
|
||||||
|
result = syntactic_implication_aux(f, g);
|
||||||
|
}
|
||||||
|
|
||||||
// Cache result
|
// Cache result
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -522,13 +522,13 @@ REALIZABLE
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 1
|
States: 1
|
||||||
Start: 0
|
Start: 0
|
||||||
AP: 3 "b" "c" "a"
|
AP: 3 "a" "b" "c"
|
||||||
acc-name: all
|
acc-name: all
|
||||||
Acceptance: 0 t
|
Acceptance: 0 t
|
||||||
properties: trans-labels explicit-labels state-acc deterministic
|
properties: trans-labels explicit-labels state-acc deterministic
|
||||||
--BODY--
|
--BODY--
|
||||||
State: 0
|
State: 0
|
||||||
[!0&!1 | !1&!2] 0
|
[!0&!2 | !1&!2] 0
|
||||||
[0&1&2] 0
|
[0&1&2] 0
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue