24.09., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

Commit b7490ae7 authored by Salomon Sickert-Zehnter's avatar Salomon Sickert-Zehnter

Merge branch 'iar-improvements' into 'master'

Iar improvements

See merge request i7/owl!351
parents cdf659ca f0044ade
......@@ -189,6 +189,15 @@
],
"data": "M"
},
"iar": {
"tools": [
"iar",
"iar#min",
"iar#odd",
"iar#min,odd"
],
"data": "M"
},
"ltl2dpa-convert": {
"tools": [
"ltl2dpa-convert#min",
......
......@@ -101,6 +101,25 @@
"optimize-aut"
]
},
"ltl2dgra2dra": {
"type": "owl",
"input": "ltl",
"output": "hoa",
"name": "ltl2dgra",
"flags": {
"asymmetric": "--asymmetric",
"symmetric": "--symmetric",
"disable-portfolio": "--disable-portfolio"
},
"pre": [
"simplify-ltl"
],
"post": [
"optimize-aut",
"dgra2dra",
"optimize-aut"
]
},
"ltl2da": {
"type": "owl",
"input": "ltl",
......@@ -169,7 +188,28 @@
"post": [
"optimize-aut",
"dgra2dra",
"dra2dpa",
"optimize-aut",
["dra2dpa", "--min"],
"optimize-aut"
]
},
"iar": {
"type": "owl",
"input": "ltl",
"output": "hoa",
"name": "dra2dpa",
"flags": {
"odd": "--odd",
"min": "--min"
},
"pre": [
"simplify-ltl",
"ltl2dgra",
"optimize-aut",
"dgra2dra",
"optimize-aut"
],
"post": [
"optimize-aut"
]
},
......@@ -211,7 +251,12 @@
"hoaf"
],
"flags": {
"hoaf": "--hoaf=1.1"
"hoaf": "--hoaf=1.1",
"deterministic": "-D",
"any": "-a",
"buchi": "-B",
"complete": "-C",
"parity": "-P"
}
},
"ltl2dpa-convert": {
......
......@@ -501,7 +501,10 @@ public final class HashMapAutomaton<S, A extends OmegaAcceptance> implements
public static <S, A extends OmegaAcceptance> HashMapAutomaton<S, A> copyOf(
Automaton<S, A> source) {
HashMapAutomaton<S, A> target = new HashMapAutomaton<>(source.factory(), source.acceptance());
source.initialStates().forEach(target::addInitialState);
MutableAutomatonUtil.copyInto(source, target);
target.trim();
target.name(source.name());
assert source.states().equals(target.states());
return target;
}
......
......@@ -72,11 +72,11 @@ public final class MutableAutomatonUtil {
return Optional.of(sinkState);
}
/**
* Copies all the states of {@code source} into {@code target}.
*/
public static <S> void copyInto(Automaton<S, ?> source, MutableAutomaton<S, ?> target) {
source.initialStates().forEach(target::addInitialState);
source.accept((Automaton.Visitor<S>) new CopyVisitor<>(target));
target.trim(); // Cannot depend on iteration order, thus we need to trim().
target.name(source.name());
}
public static final class Sink {
......
......@@ -237,7 +237,9 @@ public final class RabinDegeneralization {
}
};
resultAutomaton.addInitialState(initialSccState);
MutableAutomatonUtil.copyInto(sourceAutomaton, resultAutomaton);
resultAutomaton.trim();
var sccDecomposition2 = SccDecomposition.of(
sourceAutomaton.states(),
......
......@@ -20,6 +20,7 @@
package owl.translations.dra2dpa;
import com.google.auto.value.AutoValue;
import com.google.auto.value.extension.memoized.Memoized;
import de.tum.in.naturals.IntPreOrder;
import owl.automaton.AnnotatedState;
......@@ -30,6 +31,7 @@ public abstract class IARState<R> implements AnnotatedState<R> {
public abstract IntPreOrder record();
public static <R> IARState<R> of(R originalState) {
return of(originalState, IntPreOrder.empty());
}
......@@ -38,6 +40,11 @@ public abstract class IARState<R> implements AnnotatedState<R> {
return new AutoValue_IARState<>(originalState, record);
}
@Memoized
@Override
@SuppressWarnings("PMD.OverrideBothEqualsAndHashcode")
public abstract int hashCode();
@Override
public String toString() {
if (record().size() == 0) {
......
......@@ -54,6 +54,7 @@ import owl.automaton.Automaton;
import owl.automaton.acceptance.GeneralizedRabinAcceptance;
import owl.automaton.acceptance.OmegaAcceptance;
import owl.automaton.acceptance.OmegaAcceptanceCast;
import owl.automaton.acceptance.ParityAcceptance;
import owl.automaton.acceptance.RabinAcceptance;
import owl.automaton.acceptance.degeneralization.RabinDegeneralization;
import owl.automaton.acceptance.optimization.AcceptanceOptimizations;
......@@ -73,7 +74,6 @@ import owl.util.Statistics;
@SuppressWarnings("PMD")
class TranslationReport {
private static final LatexPrintVisitor PRINT_VISITOR = new LatexPrintVisitor(COMMON_ALPHABET);
@Disabled
......@@ -222,14 +222,14 @@ class TranslationReport {
var optimisedDra = OmegaAcceptanceCast.cast(
AcceptanceOptimizations.optimize(dra), RabinAcceptance.class);
return new IARBuilder<>(optimisedDra).build();
return new IARBuilder<>(optimisedDra, ParityAcceptance.Parity.MAX_EVEN).build();
});
var dpa_iar_symmetric = new Translator("\\Dtwo", environment -> formula -> {
var dra = SymmetricDRAConstruction.of(environment, RabinAcceptance.class, true).apply(formula);
var optimisedDra = OmegaAcceptanceCast.cast(
AcceptanceOptimizations.optimize(dra), RabinAcceptance.class);
return new IARBuilder<>(optimisedDra).build();
return new IARBuilder<>(optimisedDra, ParityAcceptance.Parity.MAX_EVEN).build();
});
// With Portfolio
......
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