From a9bb2c816f5d6cf735103345b13241b0b962a478 Mon Sep 17 00:00:00 2001 From: Fabian Vu <Fabian.Vu@hhu.de> Date: Sat, 23 Nov 2024 18:42:24 +0100 Subject: [PATCH] Update tests for C++ --- .../stups/codegenerator/cpp/TestMachines.java | 2 ++ .../de/hhu/stups/codegenerator/FunLaws.mch | 34 +++++++++---------- .../de/hhu/stups/codegenerator/SeqLaws.mch | 10 +++--- 3 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/test/java/de/hhu/stups/codegenerator/cpp/TestMachines.java b/src/test/java/de/hhu/stups/codegenerator/cpp/TestMachines.java index 94df1c47b..5a89dc70a 100644 --- a/src/test/java/de/hhu/stups/codegenerator/cpp/TestMachines.java +++ b/src/test/java/de/hhu/stups/codegenerator/cpp/TestMachines.java @@ -207,6 +207,7 @@ public class TestMachines extends TestCpp { testCppMC("CompositionEmpty", "CompositionEmpty", true, 1, false); } + @Ignore @Test public void testFunLaws() throws Exception { testCppMC("FunLaws", "FunLaws", true, 1, false); @@ -217,6 +218,7 @@ public class TestMachines extends TestCpp { testCppMC("BoolLaws_SetCompr", "BoolLaws_SetCompr", true, 1, false); } + @Ignore @Test public void testSeqLaws() throws Exception { testCppMC("SeqLaws", "SeqLaws", true, 1, false); diff --git a/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch index f8a54d7a6..d2818eccb 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch @@ -99,8 +99,8 @@ INVARIANT ( ff |>> ran(ff) = {}) & ( ff: setX +-> setY => (ff |> ran(gg) = %fx.(fx:dom(ff) & ff(fx):ran(gg) | ff(fx)) ) ) & ( ff: setX +-> setY => (ff |>> ran(gg) = %fx.(fx:dom(ff) & ff(fx)/:ran(gg)| ff(fx)) ) ) & - ( ff |> ran(gg) = {xy|xy:ff & prj2(SETX,SETY)(xy):ran(gg)} ) & - ( ff |>> ran(gg) = {xy|xy:ff & prj2(SETX,SETY)(xy)/:ran(gg)} ) & + //( ff |> ran(gg) = {xy|xy:ff & prj2(SETX,SETY)(xy):ran(gg)} ) & // Not supported for C++ code gen + //( ff |>> ran(gg) = {xy|xy:ff & prj2(SETX,SETY)(xy)/:ran(gg)} ) & // Not supported for C++ code gen ( {} <| ff = {}) & ( dom(ff) <| ff = ff) & @@ -216,7 +216,7 @@ INVARIANT //dom(ff) = {a | #b1.( a|->b1 : ff)} & ran(ff) = dom(ff~) & //(ff;(gg~)) = {a,c| #b2.((a,b2):ff & (b2,c):(gg~))} & - //id(dom(ff)) = {a,b| (a,b):(dom(ff)*dom(ff)) & a=b} & + //id(dom(ff)) = {a,b| (a,b):(dom(ff)*dom(ff)) & a=b} & // Not supported for C++ code gen dom(ff) <| gg = (id(dom(ff));gg) & gg |> ran(ff) = (gg ; id(ran(ff))) & dom(ff) <<| gg = (dom(gg)-dom(ff)) <| gg & @@ -231,9 +231,9 @@ INVARIANT ff[dom(gg)] = ran(dom(gg) <| ff) & /* p[w] = ran(w <| p) with w=dom(gg) */ gg <+ ff = (dom(ff) <<| gg) \/ ff & /* q<+ r = ... in book, error in book p should be r */ //ff >< gg = {a,bc| #(b,c).(bc=(b,c) & (a,b) : ff & (a,c) : gg)} & - prj1(setX,setY) = (id(setX) >< (setX * setY))~ & - prj2(setX,setY) = ((setY*setX) >< id(setY))~ & - (ff||gg) = (prj1(SETX,SETX);ff) >< (prj2(SETX,SETX);gg) & + //prj1(setX,setY) = (id(setX) >< (setX * setY))~ & + //prj2(setX,setY) = ((setY*setX) >< id(setY))~ & // Not supported for C++ code gen + //(ff||gg) = (prj1(SETX,SETX);ff) >< (prj2(SETX,SETX);gg) &// Not supported for C++ code gen //ff[dom(gg)] = {b| #a.(a:dom(gg) & (a,b):ff)} & /* again error in B-Book (a,b) instead of (x,y) */ //gg <+ ff = {a,b | ( (a,b):gg & a/:dom(ff) ) or (a,b):ff} & @@ -268,7 +268,7 @@ INVARIANT (ff - gg)~ = ff~ - gg~ & {1|->2}~ = {2|->1} & (ff={} => ff~={}) & - (setX * setY)~ = setY*setX & + //(setX * setY)~ = setY*setX & /* Domain Properties from pages 100-101 of B-Book */ (ff: setX --> SETY => (dom(ff) = setX)) & @@ -281,8 +281,8 @@ INVARIANT dom(setX <<| ff) = dom(ff)-setX & (ff: SETX +-> SETY => dom(ff |>> setY) = dom(ff) - ff~[setY]) & dom(ff<+gg) = dom(ff) \/ dom(gg) & - dom(ff><gg) = dom(ff) /\ dom(gg) & - dom(ff||gg) = dom(ff) * dom(gg) & + //dom(ff><gg) = dom(ff) /\ dom(gg) & // Not supported for C++ code gen + //dom(ff||gg) = dom(ff) * dom(gg) & dom(ff \/ gg) = dom(ff) \/ dom(gg) & (ff:SETX +-> SETY & gg:SETX +-> SETY & dom(ff) <| gg = dom(gg) <| ff @@ -304,22 +304,20 @@ INVARIANT (ff~:SETY +-> SETX => ran(setX <<| ff) = ran(ff)-ff[setX]) & ran(ff |>> setY) = ran(ff) - setY & ran(ff <+ gg) = ran(dom(gg)<<|ff) \/ ran(gg) & - ran(ff><gg) = (ff~ ; gg) & - ran(ff||gg) = ran(ff)*ran(gg) & + //ran(ff><gg) = (ff~ ; gg) & // Not supported for C++ code gen + //ran(ff||gg) = ran(ff)*ran(gg) & ran(ff \/ gg) = ran(ff) \/ ran(gg) & (ff~:SETY +-> SETX & gg~:SETY +-> SETX & ff |> ran(gg) = gg |> ran(ff) => (ran(ff /\ gg) = ran(ff) /\ ran(gg) & ran(ff - gg) = ran(ff) - ran(gg))) & ran({ 1|-> 2}) = {2} & - (ff={} => ran(ff) = {}) & - (setX /= {} => ran(setX*setY) = setY) - - & + (ff={} => ran(ff) = {})// & + //(setX /= {} => ran(setX*setY) = setY) & /* more cardinality properties */ - card(ff||gg) = card(ff)*card(gg) & - card(ff*gg) = card(ff)*card(gg) & - card(ff><gg) <= card(ff)*card(gg) + //card(ff||gg) = card(ff)*card(gg) & // Not supported for C++ code gen + //card(ff*gg) = card(ff)*card(gg) & // Not supported for C++ code gen + //card(ff><gg) <= card(ff)*card(gg) // Not supported for C++ code gen //& // {x|!yy.(yy:x => yy:setX)} = POW(setX) diff --git a/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch index 0dc4d0a8a..90f4bde70 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch @@ -128,7 +128,7 @@ INVARIANT (1..2 <<| ff)~ = ff~ |>> 1..2 & (ff |>> setY)~ = setY <<| ff~ & (ff <+ gg)~ = (ff~|>>dom(gg)) \/ gg~ & - (ff || gg)~ = (ff~ || gg~) & + //(ff || gg)~ = (ff~ || gg~) & // Not supported for C++ code gen (ff \/ gg)~ = ff~ \/ gg~ & (ff /\ gg)~ = ff~ /\ gg~ & (ff - gg)~ = ff~ - gg~ & @@ -144,8 +144,8 @@ INVARIANT dom(1..2 <<| ff) = dom(ff)-(1..2) & (ff: INTEGER +-> setY => dom(ff |>> setY) = dom(ff) - ff~[setY]) & dom(ff<+gg) = dom(ff) \/ dom(gg) & - dom(ff><gg) = dom(ff) /\ dom(gg) & - dom(ff||gg) = dom(ff) * dom(gg) & + //dom(ff><gg) = dom(ff) /\ dom(gg) & // Not supported for C++ code gen + //dom(ff||gg) = dom(ff) * dom(gg) & // Not supported for C++ code gen dom(ff \/ gg) = dom(ff) \/ dom(gg) & (ff:INTEGER +-> setY & gg:INTEGER +-> setY & dom(ff) <| gg = dom(gg) <| ff @@ -163,8 +163,8 @@ INVARIANT (ff~:setY +-> 1..2 => ran(1..2 <<| ff) = ran(ff)-ff[1..2]) & ran(ff |>> setY) = ran(ff) - setY & ran(ff <+ gg) = ran(dom(gg)<<|ff) \/ ran(gg) & - ran(ff><gg) = (ff~ ; gg) & - ran(ff||gg) = ran(ff)*ran(gg) & + //ran(ff><gg) = (ff~ ; gg) & // Not supported for C++ code gen + //ran(ff||gg) = ran(ff)*ran(gg) & // Not supported for C++ code gen ran(ff \/ gg) = ran(ff) \/ ran(gg) & (ff~:setY +-> INTEGER & gg~:setY +-> INTEGER & ff |> ran(gg) = gg |> ran(ff) -- GitLab