Abstract semantics of trims for FSA

lisa-analyzer · Aug 21, 2023 · 18fdb03 · 18fdb03
1 parent b9e66c9
commit 18fdb03
Show file tree

Hide file tree

Showing 3 changed files with 125 additions and 12 deletions.
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
@@ -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
@@ -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<Transition<StringSymbol>> toAdd = new HashSet<>();
+		Set<Transition<StringSymbol>> toRemove = new HashSet<>();
+
+		while (true) {
+			for (Transition<StringSymbol> t : result.getOutgoingTransitionsFrom(result.getInitialState()))
+				if (t.getSymbol().getSymbol().equals(" ")) {
+					toRemove.add(t);
+					toAdd.add(new Transition<StringSymbol>(t.getSource(), t.getDestination(), StringSymbol.EPSILON));
+				}
+
+			result.removeTransitions(toRemove);
+			result.getTransitions().addAll(toAdd);
+
+			result.minimize();
+
+			boolean b = false;
+			for (Transition<StringSymbol> t : result.getOutgoingTransitionsFrom(result.getInitialState())){
+				if (t.getSymbol().getSymbol().equals(" "))
+					b = true;
+			}
+
+			if (!b)
+				break;
+		}
+
+		return result;
+	}
+
+	public SimpleAutomaton trimRight() {
+
+		SimpleAutomaton result = copy();
+
+
+		Set<Transition<StringSymbol>> toAdd = new HashSet<>();
+		Set<Transition<StringSymbol>> toRemove = new HashSet<>();
+
+		while (true) {
+
+			for (State qf : result.getFinalStates()) {
+				for (Transition<StringSymbol> t : result.getIngoingTransitionsFrom(qf))
+					if (t.getSymbol().getSymbol().equals(" ")) {
+						toRemove.add(t);
+						toAdd.add(new Transition<StringSymbol>(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<StringSymbol> t : result.getIngoingTransitionsFrom(qf)){
+					if (t.getSymbol().equals(new StringSymbol(" ")))
+						b = true;
+				}
+			}
+
+			if (!b)
+				break;
+		}
+
+		return result;
+	}
+
+	public SimpleAutomaton trim() {
+		return trimLeft().trimRight();
+	}
 }
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
@@ -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()));
+	}
+}