fix: remove _ in action labels

pta2maude/src/ImitatorVisitor.py

@@ -70,6 +70,7 @@ class MyVisitor(ImitatorVisitor):
         parsed_synclabs = ctx.synclabs()
         if parsed_synclabs is not None and parsed_synclabs.name_list() is not None:
             synclabs = parsed_synclabs.name_list().getText().split(",")
+            synclabs = [self._sanitize_location_name(s) for s in synclabs]
 
         automaton = Automaton(self._sanitize_location_name(ctx.NAME()), synclabs)
         locations = ctx.locations()
@@ -109,15 +110,16 @@ class MyVisitor(ImitatorVisitor):
                 update = []
                 sync = None
                 if action is not None:
-                    sync = action.sync_label()
-
                     if action.updates() is not None:
                         update_list = action.updates().update_list()
                         if update_list is not None:
                             update = update_list.getText().split(",")
 
+                    sync = action.sync_label()
                     if sync is not None:
-                        sync = str(action.sync_label().NAME())
+                        sync = self._sanitize_location_name(
+                            str(action.sync_label().NAME())
+                        )
 
                 # add reset if transition points to an urgent location
                 if target in self.fresh_clocks:

pta2maude/tests/examples/fischer-intrpr.maude

@@ -4,7 +4,7 @@ mod MODEL is
   extending ANALYSIS .
 
  ops active1 active2 check1 check2 cs1 cs2 idle1 idle2 locaccess1 locaccess2 obs1 obs2 obsviolation obswaiting : -> Location [ctor] .
- ops access_1 access_2 enter_1 enter_2 exit_1 exit_2 no_access_1 no_access_2 try_1 try_2 update_1 update_2 : -> Action [ctor] .
+ ops access1 access2 enter1 enter2 exit1 exit2 noaccess1 noaccess2 try1 try2 update1 update2 : -> Action [ctor] .
  ops observer proc1 proc2 : -> Agent [ctor] .
  ops x1 x2 : -> Clock [ctor] .
  op turn : -> DVariable [ctor] .
@@ -13,46 +13,46 @@ mod MODEL is
  op Proc1 : -> Automaton .
  eq Proc1 = < proc1 |
                  (@ idle1 inv true :
-                         (when (turn = -1) local try_1 do { x1 := 0 } goto active1)),
+                         (when (turn = -1) local try1 do { x1 := 0 } goto active1)),
                  (@ active1 inv (x1 <= delta) :
-                         (when true local update_1 do { turn := 1 ; x1 := 0 } goto check1)),
+                         (when true local update1 do { turn := 1 ; x1 := 0 } goto check1)),
                  (@ check1 inv true :
-                         (when ((x1 >= gamma) and (turn = 1)) local access_1 do { nothing } goto locaccess1 ,
-                          when ((x1 >= gamma) and (turn < 1)) local no_access_1 do { nothing } goto idle1 ,
-                          when ((x1 >= gamma) and (turn > 1)) local no_access_1 do { nothing } goto idle1)),
+                         (when ((x1 >= gamma) and (turn = 1)) local access1 do { nothing } goto locaccess1 ,
+                          when ((x1 >= gamma) and (turn < 1)) local noaccess1 do { nothing } goto idle1 ,
+                          when ((x1 >= gamma) and (turn > 1)) local noaccess1 do { nothing } goto idle1)),
                  (@ locaccess1 inv true :
-                         (when true sync enter_1 do { nothing } goto cs1)),
+                         (when true sync enter1 do { nothing } goto cs1)),
                  (@ cs1 inv true :
-                         (when true sync exit_1 do { turn := -1 } goto idle1)) >
+                         (when true sync exit1 do { turn := -1 } goto idle1)) >
                 .
 
  op Proc2 : -> Automaton .
  eq Proc2 = < proc2 |
                  (@ idle2 inv true :
-                         (when (turn = -1) local try_2 do { x2 := 0 } goto active2)),
+                         (when (turn = -1) local try2 do { x2 := 0 } goto active2)),
                  (@ active2 inv (x2 <= delta) :
-                         (when true local update_2 do { turn := 2 ; x2 := 0 } goto check2)),
+                         (when true local update2 do { turn := 2 ; x2 := 0 } goto check2)),
                  (@ check2 inv true :
-                         (when ((x2 >= gamma) and (turn = 2)) local access_2 do { nothing } goto locaccess2 ,
-                          when ((x2 >= gamma) and (turn < 2)) local no_access_2 do { nothing } goto idle2 ,
-                          when ((x2 >= gamma) and (turn > 2)) local no_access_2 do { nothing } goto idle2)),
+                         (when ((x2 >= gamma) and (turn = 2)) local access2 do { nothing } goto locaccess2 ,
+                          when ((x2 >= gamma) and (turn < 2)) local noaccess2 do { nothing } goto idle2 ,
+                          when ((x2 >= gamma) and (turn > 2)) local noaccess2 do { nothing } goto idle2)),
                  (@ locaccess2 inv true :
-                         (when true sync enter_2 do { nothing } goto cs2)),
+                         (when true sync enter2 do { nothing } goto cs2)),
                  (@ cs2 inv true :
-                         (when true sync exit_2 do { turn := -1 } goto idle2)) >
+                         (when true sync exit2 do { turn := -1 } goto idle2)) >
                 .
 
  op Observer : -> Automaton .
  eq Observer = < observer |
         (@ obswaiting inv true :
-          (when true sync enter_1 do { nothing } goto obs1 ,
-           when true sync enter_2 do { nothing } goto obs2)),
+          (when true sync enter1 do { nothing } goto obs1 ,
+           when true sync enter2 do { nothing } goto obs2)),
         (@ obs1 inv true :
-             (when true sync exit_1 do { nothing } goto obswaiting ,
-              when true sync enter_2 do { nothing } goto obsviolation)),
+             (when true sync exit1 do { nothing } goto obswaiting ,
+              when true sync enter2 do { nothing } goto obsviolation)),
         (@ obs2 inv true :
-             (when true sync exit_2 do { nothing } goto obswaiting ,
-              when true sync enter_1 do { nothing } goto obsviolation)),
+             (when true sync exit2 do { nothing } goto obswaiting ,
+              when true sync enter1 do { nothing } goto obsviolation)),
         (@ obsviolation inv true : empty) >
         .