From 914826032e5b5122a0f60e73a6c973da2cb6cd96 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Thu, 1 Jul 2021 13:07:20 +0200
Subject: [PATCH] Hack in support for labels

---
 project/build.properties                    |  1 +
 src/main/scala/ostrich/Automaton.scala      | 43 ++++++++++++++++++---
 src/main/scala/ostrich/BricsAutomaton.scala |  4 ++
 src/main/scala/ostrich/Exploration.scala    |  2 +-
 4 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100644 project/build.properties

diff --git a/project/build.properties b/project/build.properties
new file mode 100644
index 0000000000..67d27a1dfe
--- /dev/null
+++ b/project/build.properties
@@ -0,0 +1 @@
+sbt.version=1.5.3
diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index 89dcd046e7..18f5b1473e 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -41,7 +41,8 @@ import scala.collection.mutable.{HashMap => MHashMap,
 
 import uuverifiers.parikh_theory.{
   Automaton => OtherAutomaton,
-  LengthCounting
+  LengthCounting,
+  SymbolicLabel
 }
 
 /**
@@ -85,6 +86,8 @@ trait Automaton {
    */
   def assertLengthConstraint(lengthTerm: Term, prover: SimpleAPI) : Unit
 
+  def toAmandaAutomaton(): OtherAutomaton
+
 }
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -154,6 +157,8 @@ trait TLabelOps[TLabel] {
    * Get representation of interval [min,max]
    */
   def interval(min : Char, max : Char) : TLabel
+
+  def labelToSymbolicLabel(label: TLabel): SymbolicLabel
 }
 
 /**
@@ -193,7 +198,7 @@ trait TLabelEnumerator[TLabel] {
  * don't have any structure and are not composite, there is a unique
  * initial state, and a set of accepting states.
  */
-trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
+trait AtomicStateAutomaton extends Automaton {
   /**
    * Type of states
    */
@@ -204,7 +209,7 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
    */
   type TLabel
 
-  type Label = TLabel
+  
 
   /**
    * Operations on labels
@@ -259,10 +264,38 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   //////////////////////////////////////////////////////////////////////////
   // Derived methods
 
+
+
+  /**
+    * I gave up and made these
+    */
+  override lazy val toAmandaAutomaton: OtherAutomaton = {
+    val parent = this
+
+    object AutomatonAdapter extends OtherAutomaton {
+      import uuverifiers.parikh_theory.AutomataTypes.{State => OtherState}
+
+      // This really is not exactly a beautiful solution but let's go.
+      val stateToIndex: Map[parent.State, OtherState] = parent.states.zipWithIndex.toMap
+      lazy val indexToState: Map[OtherState, parent.State] = stateToIndex.map(_.swap)
+
+      val initialState: OtherState = stateToIndex(parent.initialState)
+      def isAccept(s: OtherState): Boolean = parent.isAccept(indexToState(s))
+      def outgoingTransitions(from: OtherState): Iterator[(OtherState, SymbolicLabel)] =
+        parent.outgoingTransitions(indexToState(from)).map{
+          case(s, l) =>
+            (stateToIndex(s), parent.LabelOps.labelToSymbolicLabel(l))
+        }
+      def states: Iterable[OtherState] = parent.states.map(stateToIndex)
+    }
+
+    AutomatonAdapter
+  }
+
   /**
    * Iterate over all transitions
    */
-  override def transitions : Iterator[(State, TLabel, State)] =
+  def transitions : Iterator[(State, TLabel, State)] =
     for (s1 <- states.iterator; (s2, lbl) <- outgoingTransitions(s1))
     yield (s1, lbl, s2)
 
@@ -340,7 +373,7 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   }
 
   // Spare us running multiple instantiations (it might be expensive)
-  lazy private val lengthTheory = LengthCounting(IndexedSeq(this))
+  lazy private val lengthTheory = LengthCounting(IndexedSeq(toAmandaAutomaton))
 
   /**
     * Compute the length abstraction of this automaton.
diff --git a/src/main/scala/ostrich/BricsAutomaton.scala b/src/main/scala/ostrich/BricsAutomaton.scala
index 4a00349aba..407df31fd3 100644
--- a/src/main/scala/ostrich/BricsAutomaton.scala
+++ b/src/main/scala/ostrich/BricsAutomaton.scala
@@ -43,6 +43,7 @@ import scala.collection.mutable.{HashMap => MHashMap,
                                  MultiMap => MMultiMap,
                                  Set => MSet}
 import scala.jdk.CollectionConverters._
+import uuverifiers.parikh_theory.SymbolicLabel
 
 object BricsAutomaton {
   private def toBAutomaton(aut : Automaton) : BAutomaton = aut match {
@@ -212,6 +213,9 @@ object BricsTLabelOps extends TLabelOps[(Char, Char)] {
    * Get representation of interval [min,max]
    */
   def interval(min : Char, max : Char) : (Char, Char) = (min, max)
+
+  def labelToSymbolicLabel(label: (Char, Char)): SymbolicLabel =
+    SymbolicLabel(label._1, label._2)
 }
 
 class BricsTLabelEnumerator(labels: Iterator[(Char, Char)])
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 43362ca4d5..59b256adb2 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -518,7 +518,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
                                     sources : Seq[Automaton]) : Unit = {
     // FIXME cache the theory using Princess LRUcache and/or move to AutomataUtils
     // FIXME change the type to require AtomicStateAutomaton here
-    val automata = sources.map(_.asInstanceOf[AtomicStateAutomaton]).toIndexedSeq
+    val automata = sources.map(_.toAmandaAutomaton()).toIndexedSeq
     val lengthTheory = LengthCounting(automata)
 
     for (prover <- lengthProver) {