Tests on repeat, removed kleene method (duplicated)

lisa-analyzer · Jul 8, 2023 · b61aee0 · b61aee0
1 parent 1e18628
commit b61aee0
Show file tree

Hide file tree

Showing 7 changed files with 42 additions and 23 deletions.
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/RegexAutomaton.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/RegexAutomaton.java
@@ -464,6 +464,6 @@ private RegexAutomaton union(RegexAutomaton... automata) {
 	public RegexAutomaton repeat(long n) {
 		if (n == 0)
 			return emptyString();		
-		return toRegex().repeat(n).toAutomaton(this);
+		return toRegex().simplify().repeat(n).toAutomaton(this).minimize();
 	}
 }
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
@@ -410,7 +410,7 @@ public Satisfiability containsChar(char c) throws SemanticException {
 
 	public Tarsis repeat(Interval intv) throws MathNumberConversionException {
 		if (intv.isTop() || a.hasCycle())
-			return new Tarsis(a.kleene());
+			return new Tarsis(a.star());
 		else if (intv.interval.isFinite()) {
 			if (intv.interval.isSingleton())
 				return new Tarsis(a.repeat(intv.interval.getHigh().toLong()));
@@ -422,6 +422,6 @@ else if (intv.interval.isFinite()) {
 				return new Tarsis(result);
 			}
 		} else
-			return new Tarsis(a.repeat(intv.interval.getLow().toLong()).concat(a.kleene()));
+			return new Tarsis(a.repeat(intv.interval.getLow().toLong()).concat(a.star()));
 	}
 }
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/RepeatTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/RepeatTest.java
@@ -5,6 +5,8 @@
 import org.junit.Test;
 
 import it.unive.lisa.analysis.numeric.Interval;
+import it.unive.lisa.util.datastructures.regex.Atom;
+import it.unive.lisa.util.datastructures.regex.Or;
 import it.unive.lisa.util.numeric.MathNumber;
 import it.unive.lisa.util.numeric.MathNumberConversionException;
 
@@ -14,7 +16,7 @@ public class RepeatTest {
 	public void repeatSingleString() throws MathNumberConversionException {
 		RegexAutomaton abc = RegexAutomaton.string("abc");
 		RegexAutomaton abcabc = RegexAutomaton.string("abcabc");
-		RegexAutomaton abc_star = RegexAutomaton.string("abc").kleene();
+		RegexAutomaton abc_star = RegexAutomaton.string("abc").star();
 
 		Tarsis a = new Tarsis(abc);
 
@@ -37,4 +39,33 @@ public void repeatSingleString() throws MathNumberConversionException {
 		// "abc".repeat([1,+infty]) = abc(abc)*
 		assertTrue(a.repeat(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY)).getAutomaton().isEqualTo(abc.concat(abc_star)));
 	}
+
+	@Test
+	public void repeatTwoStrings() throws MathNumberConversionException {
+
+		RegexAutomaton ab_or_cd = new Or(new Atom("ab"), new Atom("cd")).toAutomaton(RegexAutomaton.emptyLang());
+		RegexAutomaton abab_or_cdcd = new Or(new Atom("abab"), new Atom("cdcd")).toAutomaton(RegexAutomaton.emptyLang());
+
+		Tarsis a = new Tarsis(ab_or_cd);
+
+		// {"ab", "cd"}.repeat(1) = {"ab", "cd"}
+		assertTrue(a.repeat(new Interval(1, 1)).getAutomaton().isEqualTo(ab_or_cd));
+
+
+		// {"ab", "cd"}.repeat(2) = {"abab", "cdcd"}
+		assertTrue(a.repeat(new Interval(2, 2)).getAutomaton().isEqualTo(abab_or_cdcd));
+
+		// {"ab", "cd"}.repeat(0) = {""}
+		assertTrue(a.repeat(new Interval(0, 0)).getAutomaton().isEqualTo(RegexAutomaton.emptyStr()));
+
+
+		// {"ab", "cd"}.repeat([1,2]) = {"ab", "cd", "abab", "cdcd"}
+		assertTrue(a.repeat(new Interval(1, 2)).getAutomaton().isEqualTo(ab_or_cd.union(abab_or_cdcd)));
+
+		// {"ab", "cd"}.repeat([0,+infty]) = (ab|cd)*
+		assertTrue(a.repeat(new Interval(MathNumber.ZERO, MathNumber.PLUS_INFINITY)).getAutomaton().isEqualTo(ab_or_cd.star()));
+
+		// {"ab", "cd"}.repeat([1,+infty]) = (ab|cd)(ab|cd)*
+		assertTrue(a.repeat(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY)).getAutomaton().isEqualTo(ab_or_cd.concat(ab_or_cd.star())));
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/automaton/Automaton.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/automaton/Automaton.java
@@ -37,7 +37,7 @@
  *                this class have on their transitions
  */
 public abstract class Automaton<A extends Automaton<A, T>, T extends TransitionSymbol<T>>
-		implements AutomataFactory<A, T> {
+implements AutomataFactory<A, T> {
 
 	/**
 	 * The states of this automaton.
@@ -1053,7 +1053,7 @@ public String prettyPrint() {
 
 				for (Transition<T> t : transitions)
 					result.append("\t").append(st).append(" [").append(t.getSymbol()).append("] -> ")
-							.append(t.getDestination()).append("\n");
+					.append(t.getDestination()).append("\n");
 			}
 		}
 
@@ -1866,17 +1866,6 @@ public A factorsChangingInitialState(State s) {
 					t.getSymbol()));
 		return from(newStates, newDelta).minimize();
 	}
-
-
-	public A kleene() {
-		SortedSet<State> newStates = new TreeSet<>(this.states);
-		SortedSet<Transition<T>> newDelta = new TreeSet<>(this.transitions);
-
-		for (State f : getFinalStates())
-			newDelta.add(new Transition<>(f, getInitialState(), epsilon()));
-
-		return from(newStates, newDelta).minimize();		
-	}
 
 	@Override
 	public int hashCode() {

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Comp.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Comp.java
@@ -32,7 +32,7 @@ public final class Comp extends RegularExpression {
 	 * @param first  the first regular expression
 	 * @param second the second regular expression
 	 */
-	Comp(RegularExpression first, RegularExpression second) {
+	public Comp(RegularExpression first, RegularExpression second) {
 		this.first = first;
 		this.second = second;
 	}
@@ -298,7 +298,6 @@ public RegularExpression repeat(long n) {
 		RegularExpression r = Atom.EPSILON;
 		for (long i = 0; i < n; i++)
 			r = new Comp(r, this);
-		r.simplify();
-		return r;
+		return r.simplify();
 	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Or.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Or.java
@@ -31,7 +31,7 @@ public final class Or extends RegularExpression {
 	 * @param first  the first regular expression
 	 * @param second the second regular expression
 	 */
-	Or(RegularExpression first, RegularExpression second) {
+	public Or(RegularExpression first, RegularExpression second) {
 		// make things deterministic: order the branches
 		if (first.compareTo(second) <= 0) {
 			this.first = first;
@@ -281,6 +281,6 @@ protected int compareToAux(RegularExpression other) {
 
 	@Override
 	public RegularExpression repeat(long n) {
-		return new Or(first.repeat(n), second.repeat(n));
+		return new Or(first.repeat(n), second.repeat(n)).simplify();
 	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Star.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Star.java
@@ -23,7 +23,7 @@ public final class Star extends RegularExpression {
 	 * 
 	 * @param op the inner regular expression
 	 */
-	Star(RegularExpression op) {
+	public Star(RegularExpression op) {
 		this.op = op;
 	}