Provide finite representation of CCS restriction/recursion nesting

This prevents crash bugs for processes such as `A = b.A \ {c}`. The solution is to flatten reached restrictions into one.
benkeks · Sep 3, 2024 · 459b6e2 · 459b6e2
1 parent 574761e
commit 459b6e2
Showing 1 changed file with 16 additions and 5 deletions.
diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/Interpreter.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/Interpreter.scala
@@ -134,13 +134,24 @@ class Interpreter[S, A, L](
         (a, p) <- semantics(procEnv)(proc)
         if !aNames.contains(toInput(a))
       } yield {
-        (a, Syntax.Restrict(names, p, pos))
+        p match {
+          case Restrict(namesC, procC, posC) =>
+            (a, Syntax.Restrict(names ++ (namesC.filterNot(names.contains(_))), procC, pos) )
+          case other =>
+            (a, Syntax.Restrict(names, p, pos))
+        }
       }
     case Syntax.ProcessName(l, pos) =>
-      semantics(procEnv)(
-        procEnv.getOrElse(
-          l.name,
-          Syntax.Prefix(l, Syntax.NullProcess(pos), pos))
+      val continuation = procEnv.getOrElse(
+        l.name,
+        Syntax.Prefix(l, Syntax.NullProcess(pos), pos)
       )
+      if (continuation == e) {
+        // direct loop
+        System.err.println(s"Unguarded recursion at ${e.position.line}")
+        List()
+      } else {
+        semantics(procEnv)(continuation)
+      }
   }
 }