Simple subset determinization algorithm

colder · Jun 14, 2012 · 120a17d · 120a17d
1 parent f685c3f
commit 120a17d
Show file tree

Hide file tree

Showing 5 changed files with 77 additions and 10 deletions.
diff --git a/src/insane/AST/CodeExtraction.scala b/src/insane/AST/CodeExtraction.scala
@@ -122,11 +122,14 @@ trait CodeExtraction extends Extractors with Contracts {
 
               RegexParser.parseString(regex) match {
                 case Some(r) =>
-                  reporter.info("Converting "+r)
-                  withDebugCounter { cnt =>
-                    dumpNFA(RegexHelpers.regexToNFA(r), "nfa-"+cnt+".dot")
+                  withDebugCounter{ cnt => 
+                    val nfa = RegexHelpers.regexToNFA(r);
+                    dumpFA(nfa, "nfa-"+cnt+".dot")
+                    val dfa = nfa.determinize
+                    dumpFA(dfa, "dfa-"+cnt+".dot")
+
+                    fun.contrEffects +:= AssertUntouched(nfa)
                   }
-                  fun.contrEffects +:= AssertUntouched(r)
                 case _ =>
                   reporter.error("Unable to parse regex: "+regex, Some(annot.pos));
               }

diff --git a/src/insane/alias/EffectRepresentations.scala b/src/insane/alias/EffectRepresentations.scala
@@ -75,8 +75,8 @@ trait EffectRepresentations extends PointToGraphsDefs with PointToEnvs {
 
   implicit def simpleSymbolStr(s: Symbol): String = s.name.toString.split("\\$").toList.last.trim
 
-  def dumpNFA[S <% String](atm: Automaton[S], dest: String) {
-    reporter.debug("Dumping NFA to "+dest+"...")
+  def dumpFA[S <% String](atm: Automaton[S], dest: String) {
+    reporter.debug("Dumping FA to "+dest+"...")
 
     new AutomatonDotConverter(atm, "EffectAutomaton", "") {
       override def transitionLabel(t: Transition[S]): String = t.label.map(s => s : String).getOrElse("\u03B5")

diff --git a/src/insane/alias/PointToAnalysis.scala b/src/insane/alias/PointToAnalysis.scala
@@ -2022,7 +2022,7 @@ trait PointToAnalysis extends PointToGraphsDefs with PointToEnvs with PointToLat
                 val r = new NFAEffectRepresentation(effect)
                 val nfa = r.getNFA
 
-                dumpNFA(nfa, safeFileName(uniqueFunctionName(fun.symbol))+"-nfa-"+i+".dot")
+                dumpFA(nfa, safeFileName(uniqueFunctionName(fun.symbol))+"-nfa-"+i+".dot")
 
                 val reg = new RegexEffectRepresentation(effect)
 

diff --git a/src/insane/utils/Automatons.scala b/src/insane/utils/Automatons.scala
@@ -26,11 +26,12 @@ object Automatons {
       this(entry, finals.toSet, new LabeledImmutableDirectedGraphImp[Option[L], State, Transition[L]](states.toSet ++ finals + entry, transitions.toSet))
 
     def this(entry: State) = 
-      this(entry, Set(), new LabeledImmutableDirectedGraphImp[Option[L], State, Transition[L]]())
+      this(entry, Set[State](), new LabeledImmutableDirectedGraphImp[Option[L], State, Transition[L]]())
 
     lazy val transitions = graph.E
     lazy val states      = graph.V
 
+    lazy val isDeterministic = transitions.groupBy(t => (t.v1, t.label)).exists(_._2.size > 1)
 
     def removeTransitions(trs: Iterable[Transition[L]]): Automaton[L] = {
       var newGraph = trs.foldLeft(graph)((g, e) => g - e)
@@ -65,6 +66,69 @@ object Automatons {
       removeStates(states -- markedStates)
     }
 
+    def negation: Automaton[L] = {
+      val dfa = if (isDeterministic) {
+        this
+      } else {
+        this.determinize
+      }
+
+      dfa.copy(finals = dfa.states -- dfa.finals)
+    }
+
+    def determinize: Automaton[L] = {
+      def f(ss: Set[State]): Set[State] = ss.flatMap(s => Set(s) ++ graph.outs(s).collect{ case Transition(_, None, to) => to})
+
+      val alph = transitions.map(_.label).toSet
+
+
+      var statesCache = Map[Set[State], State]()
+      def realState(ss: Set[State]): State = statesCache.getOrElse(ss, {
+        val s = newState
+        statesCache += ss -> s
+        s
+      })
+
+      var dStates      = Set[State]()
+      var entry        = f(Set(this.entry))
+      var dEntry       = realState(entry)
+      var dFinals      = Set[State]()
+      var dTransitions = Set[Transition[L]]()
+      var todo         = Set[Set[State]](entry)
+      var done         = Set[Set[State]]()
+
+      while(!todo.isEmpty) {
+        val ds = todo.head
+
+        for ((a, tos) <- ds.flatMap(graph.outs(_).filter(!_.label.isEmpty)).groupBy(t => t.label).mapValues(_.map(_.v2))) {
+          val newDs = f(tos)
+
+          dStates       += realState(newDs)
+          dTransitions  += Transition(realState(ds), a, realState(newDs))
+
+          if (!done(newDs)) {
+            todo        += newDs
+          }
+        }
+        if (!(ds & this.finals).isEmpty) {
+          dFinals += realState(ds)
+        }
+
+        todo -= ds
+        done += ds
+      }
+
+      new Automaton[L](dStates, dTransitions, dEntry, dFinals)
+    }
+
+    def union(that: Automaton[L]): Automaton[L] = {
+      this
+    }
+
+    def intersection(that: Automaton[L]): Automaton[L] = {
+      this
+    }
+
     case class StateSig(ins: Set[(State, Option[L])], outs: Set[(State, Option[L])])
 
     object StateSig {

diff --git a/src/insane/utils/Contracts.scala b/src/insane/utils/Contracts.scala
@@ -2,7 +2,7 @@ package insane
 package utils
 
 import scala.tools.nsc._
-import RegularExpressions._
+import Automatons._
 
 trait Contracts {
   val global: Global
@@ -23,5 +23,5 @@ trait Contracts {
 
   abstract class EffectsContract;
 
-  case class AssertUntouched(region: Regex[String]) extends EffectsContract;
+  case class AssertUntouched(region: Automaton[String]) extends EffectsContract;
 }