toFSA fixed, repeat method for FSA

lisa-analyzer · Aug 21, 2023 · 2028460 · 2028460
1 parent 9d23332
commit 2028460
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 5 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
@@ -4,6 +4,7 @@
 import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
+import it.unive.lisa.analysis.numeric.Interval;
 import it.unive.lisa.analysis.representation.DomainRepresentation;
 import it.unive.lisa.analysis.representation.StringRepresentation;
 import it.unive.lisa.analysis.string.ContainsCharProvider;
@@ -21,6 +22,8 @@
 import it.unive.lisa.util.datastructures.automaton.Transition;
 import it.unive.lisa.util.numeric.IntInterval;
 import it.unive.lisa.util.numeric.MathNumber;
+import it.unive.lisa.util.numeric.MathNumberConversionException;
+
 import java.util.HashSet;
 import java.util.Objects;
 import java.util.Set;
@@ -421,4 +424,8 @@ public Satisfiability containsChar(char c) throws SemanticException {
 	public FSA trim() {
 		return new FSA(this.a.trim());
 	}
+
+	public FSA repeat(Interval i) throws MathNumberConversionException {
+		return new FSA(this.a.repeat(i));
+	}
 }
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
@@ -420,8 +420,12 @@ public SimpleAutomaton connectAutomaton(SimpleAutomaton second, SortedSet<State>
 			}
 
 			states.remove(secondMapping.get(second.getInitialState()));
+			secondMapping.remove(second.getInitialState());
 
 			for (Transition<StringSymbol> t : second.getTransitions()) {
+				if (t.getSource().equals(second.getInitialState()) || t.getDestination().equals(second.getInitialState()) || !secondMapping.containsKey(t.getSource()) || !secondMapping.containsKey(t.getDestination()))
+					continue;
+
 				if (!t.getSource().isInitial() && !t.getDestination().isInitial()) {
 					delta.add(new Transition<>(secondMapping.get(t.getSource()), secondMapping.get(t.getDestination()),
 							t.getSymbol()));
@@ -441,10 +445,9 @@ public SimpleAutomaton connectAutomaton(SimpleAutomaton second, SortedSet<State>
 					delta.add(new Transition<>(firstMapping.get(s), secondMapping.get(t.getDestination()),
 							t.getSymbol()));
 				}
-			}
-
+			}	
 		}
-
+		
 		return new SimpleAutomaton(states, delta);
 	}
 }
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/Tarsis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/Tarsis.java
@@ -387,8 +387,8 @@ public FSA toFSA() {
 						new StringSymbol(t.getSymbol().toString())));
 			else {
 				for (char c = 32; c <= 123; c++)
-					fsaDelta.add(new Transition<>(t.getSource(), t.getSource(), new StringSymbol(c)));
-				fsaDelta.add(new Transition<>(t.getSource(), t.getSource(), StringSymbol.EPSILON));
+					fsaDelta.add(new Transition<>(t.getSource(), t.getDestination(), new StringSymbol(c)));
+				fsaDelta.add(new Transition<>(t.getSource(), t.getDestination(), StringSymbol.EPSILON));
 			}
 		}