From 2028460493ca3ff54b8f39d15976d401a42b54dd Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Mon, 21 Aug 2023 16:29:55 +0200 Subject: [PATCH] toFSA fixed, repeat method for FSA --- .../main/java/it/unive/lisa/analysis/string/fsa/FSA.java | 7 +++++++ .../unive/lisa/analysis/string/fsa/SimpleAutomaton.java | 9 ++++++--- .../it/unive/lisa/analysis/string/tarsis/Tarsis.java | 4 ++-- 3 files changed, 15 insertions(+), 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 index 9255acea1..4ff443c94 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 @@ -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 index 6daccc5b3..507fbb3e8 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 @@ -420,8 +420,12 @@ public SimpleAutomaton connectAutomaton(SimpleAutomaton second, SortedSet } states.remove(secondMapping.get(second.getInitialState())); + secondMapping.remove(second.getInitialState()); for (Transition 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 delta.add(new Transition<>(firstMapping.get(s), secondMapping.get(t.getDestination()), t.getSymbol())); } - } - + } } - + return new SimpleAutomaton(states, delta); } } \ No newline at end of file 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 index 710edb96d..e23610b42 100644 --- 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)); } }