CInterface Fixes.

- Ensure that the input formula is in negation normal form before passing it to the subsequent automaton constructions.
- Catch the IllegalArgumentException if there are too many fixpoints to consider.
parent fcfba200
......@@ -76,6 +76,7 @@ import owl.ltl.Conjunction;
import owl.ltl.Disjunction;
import owl.ltl.EquivalenceClass;
import owl.ltl.LabelledFormula;
import owl.ltl.SyntacticFragment;
import owl.ltl.SyntacticFragments;
import owl.translations.canonical.DeterministicConstructions;
import owl.translations.canonical.DeterministicConstructionsPortfolio;
......@@ -467,9 +468,11 @@ public final class CAutomaton {
}
static DeterministicAutomatonWrapper<?, ?> of(LabelledFormula formula) {
if (SyntacticFragments.isSafety(formula.formula())) {
var nnfFormula = SyntacticFragment.NNF.contains(formula) ? formula : formula.nnf();
if (SyntacticFragments.isSafety(nnfFormula.formula())) {
return new DeterministicAutomatonWrapper<>(
DeterministicConstructionsPortfolio.safety(CInterface.ENVIRONMENT, formula),
DeterministicConstructionsPortfolio.safety(CInterface.ENVIRONMENT, nnfFormula),
SAFETY, AllAcceptance.class,
EquivalenceClass::isTrue,
Function.identity(),
......@@ -478,9 +481,9 @@ public final class CAutomaton {
);
}
if (SyntacticFragments.isCoSafety(formula.formula())) {
if (SyntacticFragments.isCoSafety(nnfFormula.formula())) {
return new DeterministicAutomatonWrapper<>(
DeterministicConstructionsPortfolio.coSafety(CInterface.ENVIRONMENT, formula),
DeterministicConstructionsPortfolio.coSafety(CInterface.ENVIRONMENT, nnfFormula),
Acceptance.CO_SAFETY, BuchiAcceptance.class,
EquivalenceClass::isTrue,
Function.identity(),
......@@ -489,39 +492,39 @@ public final class CAutomaton {
);
}
var formulasConj = formula.formula() instanceof Conjunction
? formula.formula().operands
: Set.of(formula.formula());
var formulasConj = nnfFormula.formula() instanceof Conjunction
? nnfFormula.formula().operands
: Set.of(nnfFormula.formula());
if (formulasConj.stream().allMatch(SyntacticFragments::isGfCoSafety)) {
return new DeterministicAutomatonWrapper<>(
DeterministicConstructionsPortfolio.gfCoSafety(CInterface.ENVIRONMENT, formula, false),
DeterministicConstructionsPortfolio.gfCoSafety(CInterface.ENVIRONMENT, nnfFormula, false),
BUCHI, GeneralizedBuchiAcceptance.class,
x -> false,
x -> formula,
x -> nnfFormula,
x -> x.inSet(0) ? 1.0d : 0.5d,
-1
);
}
var formulasDisj = formula.formula() instanceof Disjunction
? formula.formula().operands
: Set.of(formula.formula());
var formulasDisj = nnfFormula.formula() instanceof Disjunction
? nnfFormula.formula().operands
: Set.of(nnfFormula.formula());
if (formulasDisj.stream().allMatch(SyntacticFragments::isFgSafety)) {
return new DeterministicAutomatonWrapper<>(
DeterministicConstructionsPortfolio.fgSafety(CInterface.ENVIRONMENT, formula, false),
DeterministicConstructionsPortfolio.fgSafety(CInterface.ENVIRONMENT, nnfFormula, false),
CO_BUCHI, GeneralizedCoBuchiAcceptance.class,
x -> false,
x -> formula,
x -> nnfFormula,
x -> x.inSet(0) ? 0.0d : 0.5d,
-1
);
}
if (SyntacticFragments.isSafetyCoSafety(formula.formula())) {
if (SyntacticFragments.isSafetyCoSafety(nnfFormula.formula())) {
return new DeterministicAutomatonWrapper<>(
DeterministicConstructionsPortfolio.safetyCoSafety(CInterface.ENVIRONMENT, formula),
DeterministicConstructionsPortfolio.safetyCoSafety(CInterface.ENVIRONMENT, nnfFormula),
BUCHI, BuchiAcceptance.class,
x -> x.all().isFalse() && x.all().isFalse(),
DeterministicConstructions.BreakpointStateRejecting::all,
......@@ -530,9 +533,9 @@ public final class CAutomaton {
);
}
if (SyntacticFragments.isCoSafetySafety(formula.formula())) {
if (SyntacticFragments.isCoSafetySafety(nnfFormula.formula())) {
return new DeterministicAutomatonWrapper<>(
DeterministicConstructionsPortfolio.coSafetySafety(CInterface.ENVIRONMENT, formula),
DeterministicConstructionsPortfolio.coSafetySafety(CInterface.ENVIRONMENT, nnfFormula),
CO_BUCHI, CoBuchiAcceptance.class,
x -> x.all().isTrue() && x.accepting().isTrue(),
DeterministicConstructions.BreakpointStateAccepting::all,
......@@ -544,7 +547,7 @@ public final class CAutomaton {
var function = new LTL2DPAFunction(CInterface.ENVIRONMENT,
EnumSet.of(COMPLEMENT_CONSTRUCTION_HEURISTIC));
Automaton<AnnotatedState<EquivalenceClass>, ParityAcceptance> automaton =
(Automaton) function.apply(formula);
(Automaton) function.apply(nnfFormula);
if (automaton.acceptance().parity() == ParityAcceptance.Parity.MIN_ODD) {
return new DeterministicAutomatonWrapper<>(
......
......@@ -33,6 +33,7 @@ import java.util.Objects;
import java.util.Optional;
import java.util.concurrent.atomic.AtomicReference;
import java.util.function.Function;
import java.util.function.IntSupplier;
import java.util.function.Supplier;
import owl.automaton.AnnotatedStateOptimisation;
import owl.automaton.Automaton;
......@@ -81,12 +82,16 @@ public class LTL2DPAFunction implements Function<LabelledFormula, Automaton<?, P
if (configuration.contains(COMPLEMENT_CONSTRUCTION_HEURISTIC)) {
int fixpoints = configuration.contains(SYMMETRIC)
? Selector.selectSymmetric(formula.formula(), false).size()
: Selector.selectAsymmetric(formula.formula(), false).size();
? getOrMaxInt(() -> Selector.selectSymmetric(formula.formula(), false).size())
: getOrMaxInt(() -> Selector.selectAsymmetric(formula.formula(), false).size());
int negationFixpoints = configuration.contains(SYMMETRIC)
? Selector.selectSymmetric(formula.formula().not(), false).size()
: Selector.selectAsymmetric(formula.formula().not(), false).size();
? getOrMaxInt(() -> Selector.selectSymmetric(formula.formula().not(), false).size())
: getOrMaxInt(() -> Selector.selectAsymmetric(formula.formula().not(), false).size());
if (fixpoints == Integer.MAX_VALUE && negationFixpoints == Integer.MAX_VALUE) {
throw new IllegalStateException("Too many fixpoints.");
}
if (fixpoints <= negationFixpoints) {
automatonSupplier = configuration.contains(SYMMETRIC)
......@@ -213,4 +218,12 @@ public class LTL2DPAFunction implements Function<LabelledFormula, Automaton<?, P
.deterministicComplement(automaton, sinkState, ParityAcceptance.class);
}
}
private static int getOrMaxInt(IntSupplier supplier) {
try {
return supplier.getAsInt();
} catch (IllegalArgumentException ex) {
return Integer.MAX_VALUE;
}
}
}
......@@ -19,6 +19,7 @@
package owl.cinterface;
import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
import static org.junit.jupiter.api.Assertions.assertTimeout;
import java.time.Duration;
......@@ -27,13 +28,14 @@ import javax.annotation.Nullable;
import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.Disabled;
import org.junit.jupiter.api.Test;
import owl.cinterface.CAutomaton.DeterministicAutomatonWrapper;
import owl.ltl.parser.LtlParser;
class DeterministicAutomatonWrapperTest {
@SuppressWarnings("PMD.UnusedFormalParameter")
private static void assertEquals(
CAutomaton.DeterministicAutomatonWrapper<?, ?> automaton,
DeterministicAutomatonWrapper<?, ?> automaton,
int state,
@Nullable int[] filter,
int[] expectedTreeBuffer,
......@@ -57,14 +59,14 @@ class DeterministicAutomatonWrapperTest {
var formula6 = LtlParser.parse("G (r -> F g)", List.of("r", "g"));
var formula7 = LtlParser.parse("(G F a) | (G F b)", List.of("a", "b"));
var automaton0 = CAutomaton.DeterministicAutomatonWrapper.of(formula0);
var automaton1 = CAutomaton.DeterministicAutomatonWrapper.of(formula1);
var automaton2 = CAutomaton.DeterministicAutomatonWrapper.of(formula2);
var automaton3 = CAutomaton.DeterministicAutomatonWrapper.of(formula3);
var automaton4 = CAutomaton.DeterministicAutomatonWrapper.of(formula4);
var automaton5 = CAutomaton.DeterministicAutomatonWrapper.of(formula5);
var automaton6 = CAutomaton.DeterministicAutomatonWrapper.of(formula6);
var automaton7 = CAutomaton.DeterministicAutomatonWrapper.of(formula7);
var automaton0 = DeterministicAutomatonWrapper.of(formula0);
var automaton1 = DeterministicAutomatonWrapper.of(formula1);
var automaton2 = DeterministicAutomatonWrapper.of(formula2);
var automaton3 = DeterministicAutomatonWrapper.of(formula3);
var automaton4 = DeterministicAutomatonWrapper.of(formula4);
var automaton5 = DeterministicAutomatonWrapper.of(formula5);
var automaton6 = DeterministicAutomatonWrapper.of(formula6);
var automaton7 = DeterministicAutomatonWrapper.of(formula7);
assertEquals(automaton0, 0, null,
new int[]{}, new int[]{-2, -1}, new double[]{1.0d});
......@@ -95,7 +97,7 @@ class DeterministicAutomatonWrapperTest {
@Disabled
@Test
void testMaskedEdges() {
var automaton = CAutomaton.DeterministicAutomatonWrapper
var automaton = DeterministicAutomatonWrapper
.of(LtlParser.parse("a | b", List.of("a", "b")));
assertEquals(automaton, 0, new int[]{0, -1, -2},
......@@ -127,8 +129,8 @@ class DeterministicAutomatonWrapperTest {
+ "& X G (w | x | y)");
Assertions.assertEquals(25, formula.atomicPropositions().size());
var instance1 = CAutomaton.DeterministicAutomatonWrapper.of(formula);
var instance2 = CAutomaton.DeterministicAutomatonWrapper.of(formula.not());
var instance1 = DeterministicAutomatonWrapper.of(formula);
var instance2 = DeterministicAutomatonWrapper.of(formula.not());
var edgeTree = instance1.edgeTree(0, true);
Assertions.assertEquals(66, edgeTree.tree.size());
......@@ -137,4 +139,9 @@ class DeterministicAutomatonWrapperTest {
Assertions.assertEquals(66, edgeTree.tree.size());
});
}
@Test
void testFormulaNotInNnf() {
assertDoesNotThrow(() -> DeterministicAutomatonWrapper.of(LtlParser.parse("a <-> b")));
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment