diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java index 7433e4cce..feae68c58 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java @@ -1,5 +1,11 @@ package it.unive.lisa.analysis.string.fsa; +import java.util.HashSet; +import java.util.Objects; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; + import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; @@ -21,11 +27,6 @@ import it.unive.lisa.util.datastructures.automaton.Transition; import it.unive.lisa.util.numeric.IntInterval; import it.unive.lisa.util.numeric.MathNumber; -import java.util.HashSet; -import java.util.Objects; -import java.util.Set; -import java.util.SortedSet; -import java.util.TreeSet; /** * A class that represent the Finite State Automaton domain for strings, @@ -373,7 +374,7 @@ public FSA replace(FSA search, FSA repl) { return TOP; } } - + @Override public Satisfiability containsChar(char c) throws SemanticException { if (isTop()) @@ -417,4 +418,8 @@ public Satisfiability containsChar(char c) throws SemanticException { return Satisfiability.NOT_SATISFIED; } + + public FSA trim() { + return new FSA(this.a.trim()); + } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/SimpleAutomaton.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/SimpleAutomaton.java index 76cda7128..84bb4e457 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/SimpleAutomaton.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/SimpleAutomaton.java @@ -1,18 +1,20 @@ package it.unive.lisa.analysis.string.fsa; -import it.unive.lisa.util.datastructures.automaton.Automaton; -import it.unive.lisa.util.datastructures.automaton.CyclicAutomatonException; -import it.unive.lisa.util.datastructures.automaton.State; -import it.unive.lisa.util.datastructures.automaton.Transition; -import it.unive.lisa.util.datastructures.regex.Atom; -import it.unive.lisa.util.datastructures.regex.RegularExpression; import java.util.Collections; +import java.util.HashSet; import java.util.Optional; import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; import java.util.stream.Collectors; +import it.unive.lisa.util.datastructures.automaton.Automaton; +import it.unive.lisa.util.datastructures.automaton.CyclicAutomatonException; +import it.unive.lisa.util.datastructures.automaton.State; +import it.unive.lisa.util.datastructures.automaton.Transition; +import it.unive.lisa.util.datastructures.regex.Atom; +import it.unive.lisa.util.datastructures.regex.RegularExpression; + /** * A class that describes an generic automaton(dfa, nfa, epsilon nfa) using a * standard alphabet of single characters. @@ -180,4 +182,78 @@ public SimpleAutomaton replace(SimpleAutomaton toReplace, SimpleAutomaton str) t result = result.union(new SimpleAutomaton(a.replace(b, c))); return result; } + + public SimpleAutomaton trimLeft() { + SimpleAutomaton result = copy(); + + Set> toAdd = new HashSet<>(); + Set> toRemove = new HashSet<>(); + + while (true) { + for (Transition t : result.getOutgoingTransitionsFrom(result.getInitialState())) + if (t.getSymbol().getSymbol().equals(" ")) { + toRemove.add(t); + toAdd.add(new Transition(t.getSource(), t.getDestination(), StringSymbol.EPSILON)); + } + + result.removeTransitions(toRemove); + result.getTransitions().addAll(toAdd); + + result.minimize(); + + boolean b = false; + for (Transition t : result.getOutgoingTransitionsFrom(result.getInitialState())){ + if (t.getSymbol().getSymbol().equals(" ")) + b = true; + } + + if (!b) + break; + } + + return result; + } + + public SimpleAutomaton trimRight() { + + SimpleAutomaton result = copy(); + + + Set> toAdd = new HashSet<>(); + Set> toRemove = new HashSet<>(); + + while (true) { + + for (State qf : result.getFinalStates()) { + for (Transition t : result.getIngoingTransitionsFrom(qf)) + if (t.getSymbol().getSymbol().equals(" ")) { + toRemove.add(t); + toAdd.add(new Transition(t.getSource(), t.getDestination(), StringSymbol.EPSILON)); + } + } + + result.removeTransitions(toRemove); + result.getTransitions().addAll(toAdd); + + result.minimize(); + + boolean b = false; + for (State qf : result.getFinalStates()) { + + for (Transition t : result.getIngoingTransitionsFrom(qf)){ + if (t.getSymbol().equals(new StringSymbol(" "))) + b = true; + } + } + + if (!b) + break; + } + + return result; + } + + public SimpleAutomaton trim() { + return trimLeft().trimRight(); + } } \ No newline at end of file diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/TrimTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/TrimTest.java new file mode 100644 index 000000000..e779fcf3a --- /dev/null +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/TrimTest.java @@ -0,0 +1,32 @@ +package it.unive.lisa.analysis.string.fsa; + +import static org.junit.Assert.assertTrue; + +import org.junit.Test; + +public class TrimTest { + + @Test + public void test01() { + SimpleAutomaton a = new SimpleAutomaton(" a "); + assertTrue(a.trim().isEqualTo(new SimpleAutomaton("a"))); + } + + @Test + public void test02() { + SimpleAutomaton b = new SimpleAutomaton(" a ").union(new SimpleAutomaton(" b ")); + assertTrue(b.trim().isEqualTo(new SimpleAutomaton("a").union(new SimpleAutomaton("b")))); + } + + @Test + public void test03() { + SimpleAutomaton c = new SimpleAutomaton("a").union(new SimpleAutomaton(" b ")); + assertTrue(c.trim().isEqualTo(new SimpleAutomaton("a").union(new SimpleAutomaton("b")))); + } + + @Test + public void test04() { + SimpleAutomaton c = new SimpleAutomaton(" a ").star(); + assertTrue(c.trim().isEqualTo(new SimpleAutomaton("a").star())); + } +}