diff --git a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java index 7b7ecba586cb5f0eab2ae94ffb33a38c01263b09..6b4f08cdc80746bcb0eff1cbf943b3fd1123a0a8 100644 --- a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java +++ b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java @@ -264,4 +264,26 @@ public class ActionsTest { compare("MACHINE Testing END", module); } + + @Test + @Ignore("not implemented yet, one operation in the disjunction is ignored") + public void testOperationsWithSameName() throws Exception { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Naturals \n" + + "VARIABLES x \n" + + "Init == x = 1 \n" + + "Op(y) == x' = y \n" + + "Next == \\/ Op(2) \n" + + " \\/ Op(3) \n" + + "================================="; + + final String expected = "MACHINE Testing\n" + + "VARIABLES x\n" + + "INVARIANT x : INTEGER \n" + + "INITIALISATION x:(x = 1) \n" + + "OPERATIONS \n" + + " Op(y) = SELECT y : {2,3} THEN x := y END \n" + + "END"; + compare(expected, module); + } }