Add renaming / syntax for CSP style hiding

benkeks · Sep 3, 2024 · 423bf65 · 423bf65
1 parent 459b6e2
commit 423bf65
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 3 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
@@ -141,6 +141,19 @@ class Interpreter[S, A, L](
             (a, Syntax.Restrict(names, p, pos))
         }
       }
+    case Syntax.Renaming(rns, proc, pos) =>
+      val aRns = rns.map { case (from, to) => (arrowLabeling(Some(from)).get, arrowLabeling(Some(to)).get) }
+      for {
+        (a, p) <- semantics(procEnv)(proc)
+      } yield {
+        val action = aRns.find(_._1 == a).map(_._2).getOrElse(a)
+        p match {
+          case Syntax.Renaming(rnsC, procC, posC) =>
+            (action, Syntax.Renaming(rns ++ (rnsC.filterNot { case (from, to) => rns.contains(from) } ), procC, pos) )
+          case other =>
+            (action, Syntax.Renaming(rns, p, pos))
+        }
+      }
     case Syntax.ProcessName(l, pos) =>
       val continuation = procEnv.getOrElse(
         l.name,

diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/Parser.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/Parser.scala
@@ -199,6 +199,11 @@ class Parser(val input: String) extends Parsing {
             case (labels, rt) =>
               ParseSuccess(Restrict(labels, proc, proc.position), rt)
           }
+        case Backslash(_) :: Identifier("csp", p) :: CurlyBracketOpen(_) :: in5 =>
+          parseLabelSet(in5) flatMap {
+            case (labels, rt) =>
+              ParseSuccess(Renaming(labels.map(l => (l, Label("tau", p))), proc, proc.position), rt)
+          }
         case other =>
           ParseFail("Expected process continuation.", other)
       }

diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/PrettyPrinter.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/PrettyPrinter.scala
@@ -37,7 +37,14 @@ class PrettyPrinter {
     case Parallel(procs, pos) =>
       procs.map(show(_)).mkString("(", " | ", ")")
     case Restrict(names, proc, pos) =>
-      show(proc) + " \\ " + names.map(show(_)).mkString("{", ", ", "}") 
+      show(proc) + " \\ " + names.map(show(_)).mkString("{", ", ", "}")
+    case Renaming(renamings, proc, pos) =>
+      val renamingString = if (renamings.forall(_._2.name == "tau")) {
+        renamings.map(_._1).mkString(" \\csp {",",","}")
+      } else {
+        renamings.map { case (from, to) => s"$from -> $to" }.mkString("[", ",", "]")
+      }
+      show(proc) + renamingString
     case ProcessName(l, p0) =>
       show(l)
     case Label(l, p0) =>

diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/Syntax.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/Syntax.scala
@@ -21,6 +21,7 @@ object Syntax {
       case Label(n, p0) => Label(n, pos)
       case Prefix(l, proc, p0) => Prefix(l, proc, pos)
       case Restrict(lls, proc, p0) => Restrict(lls, proc, pos)
+      case Renaming(rns, proc, p0) => Renaming(rns, proc, pos)
       case Parallel(procs, p0) => Parallel(procs, pos)
       case Choice(procs, p0) => Choice(procs, pos)
       case ProcessName(l, p0) => ProcessName(l, pos)
@@ -35,6 +36,7 @@ object Syntax {
         case Label(n, p0) => Label(n, Pos0)
         case Prefix(l, proc, p0) => Prefix(l, proc.prunePos, Pos0)
         case Restrict(lls, proc, p0) => Restrict(lls, proc.prunePos, Pos0)
+        case Renaming(rns, proc, p0) => Renaming(rns, proc.prunePos, Pos0)
         case Parallel(procs, p0) => Parallel(procs map (_.prunePos), Pos0)
         case Choice(procs, p0) => Choice(procs map (_.prunePos), Pos0)
         case ProcessName(l, p0) => ProcessName(l, Pos0)
@@ -97,14 +99,27 @@ object Syntax {
     }
   }
 
-    case class Restrict(val names: List[Label], val proc: ProcessExpression, pos: Pos = Pos0) extends ProcessExpression(pos) {
-    
+  case class Restrict(val names: List[Label], val proc: ProcessExpression, pos: Pos = Pos0) extends ProcessExpression(pos) {
+
     override def toString() = {
       val ps = proc.toString()
       (if (ps.contains(" ")) "(" + ps + ")" else ps) + names.mkString(" \\ {",",","}")
     }
   }
 
+  case class Renaming(val renamings: List[(Label, Label)], val proc: ProcessExpression, pos: Pos = Pos0) extends ProcessExpression(pos) {
+
+    override def toString() = {
+      val ps = proc.toString()
+      val renamingString = if (renamings.forall(_._2.name == "tau")) {
+        renamings.map(_._1).mkString(" \\csp {",",","}")
+      } else {
+        renamings.map { case (from, to) => s"$from -> $to" }.mkString("[", ",", "]")
+      }
+      (if (ps.contains(" ")) "(" + ps + ")" else ps) + renamingString
+    }
+  }
+
   case class ProcessName(val l: Label, pos: Pos = Pos0) extends ProcessExpression(pos) {
     override def toString() = l.toString
   }