Illustrate negation bug in testkf/epi1-test2

epik.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 7ea7e9dd10450bf53bdf01a8e019340d8ff7cdfad5ed5c32b98816c2900efa9f
+-- hash: ab9f441946e24e080c0327fbabc1d8c531eb79d7693ac70bc49e1f8bf73c9a21
 
 name:           epik
 version:        0.1.0.0
@@ -43,6 +43,7 @@ library
     , base >=4.7 && <5
     , containers
     , mtl
+    , stack
     , universe
     , universe-base
   default-language: Haskell2010
@@ -60,6 +61,7 @@ executable epik-exe
     , containers
     , epik
     , mtl
+    , stack
     , universe
     , universe-base
   default-language: Haskell2010
@@ -78,6 +80,7 @@ test-suite epik-test
     , containers
     , epik
     , mtl
+    , stack
     , universe
     , universe-base
   default-language: Haskell2010

examples/epi2.k

@@ -78,15 +78,17 @@ query only_peek = peek*
 query three_no_announce = three & no_announce
 
 -- 17b. Worlds of length three where only peeks have happened.
+-- Note that H/T consistency is imposed.
 -- GOOD even though it should be equivalent to 17a.
 
 query three_only_peek = three & only_peek
 
 -- 17c. Worlds of length three some announcements have happened.
--- The worlds have length three, but
+-- three & have_announce
 -- GOOD apparently
 
-query three_no_announce = three & have_announce
+query three_have_announce = three & have_announce
+
 
 
 

package.yaml

@@ -26,6 +26,7 @@ dependencies:
 - mtl
 - universe
 - universe-base
+- stack
 
 library:
   source-dirs: src

src/GuardedStrings.hs

@@ -102,7 +102,9 @@ listFuse xs ys = mapMaybe (uncurry fuse) (xs +*+ ys)
 xs +<>+ ys = xs `listFuse` ys
 
 elemApprox :: GuardedString -> [GuardedString] -> Bool
-elemApprox g = elemLeqLen (200*gsLen g) g
+
+-- Mats changed this from 200 to 3200 to increase resolution
+elemApprox g = elemLeqLen (3200*gsLen g) g
 
 elemLeqLen :: Integer -> GuardedString -> [GuardedString] -> Bool
 elemLeqLen _ _ [] = False

testkf/Bug

@@ -0,0 +1,52 @@
+* Test file
+
+epi1.k is the basic Epik program.
+test2.base has test examples. Note that test2.k and test2.fst are generated, don't edit them.
+
+Assemble them into epi1-test4.k with this.
+   make epi1-test2.k
+
+* Execution in Epik
+Go to the parent directory, and say this.
+
+   make testkf/epi1-test2.k.out
+
+* Execution in Fst
+In this directory, say this.
+  make epi1-test2.fst.out
+
+* We are getting different results with Epik and Fst for this test item.
+
+Haskell
+-- 9b. Bob knows that Aly knows that Aly peeked T in the first step
+-- The result should be aly_peek_T;announce_T + aly_peek_T.bob_peek_T.
+-- Aly peeks T in the first event and Bob figures it out in the second event.
+-- (Two & ~bob(~~aly(~(aly_peek_T ; _))))
+Example9b identifies the following strings:
+
+	aly_peek_T.announce_T.
+	aly_peek_T.aly_peek_T.
+	aly_peek_T.bob_peek_T.
+
+Fst
+-- 9b. Bob knows that Aly knows that Aly peeked T in the first step
+-- The result should be aly_peek_T;announce_T + aly_peek_T.bob_peek_T.
+-- Aly peeks T in the first event and Bob figures it out in the second event.
+-- (Two & Box(Rb,Box(Ra,Cn(World(aly_peek_T),Event))))
+
+T aly_peek_T T announce_T T
+T aly_peek_T T bob_peek_T T
+
+The world aly_peek_T.aly_peek_T in the Haskell Epik result is wrong, in this world Bob doesn't
+learn that Aly peeked T in the first event.
+
+* On the theory that the problem comes from the approximation in calculating negations, Mats experimented with adjusting this parameter in
+GuardedStrings.hs.
+
+-- Mats changed this from 200 to 3200 to increase resolution
+elemApprox g = elemLeqLen (3200*gsLen g) g
+
+It didn't resolve the bug.
+
+
+

testkf/Makefile

@@ -1,5 +1,6 @@
 test1.fm4: fst.m4 test1.base
 	cat fst.m4 test1.base > test1.fm4
+
 test1.km4: k.m4 test1.base
 	cat k.m4 test1.base > test1.km4
 

testkf/epi1-test2.fst

@@ -281,7 +281,7 @@ echo -- Event
 regex One;
 print words
 echo -------------------------------------
-;
+
 
 echo -- Two events.
 define Two Cn(Event,Event);
@@ -360,7 +360,8 @@ echo -------------------------------------
 
 
 echo -- 9b. Bob knows that Aly knows that Aly peeked T in the first step
-echo -- The result should be bob_peek_H.announce_H + bob_peek_H.aly_peek_H
+echo -- The result should be aly_peek_T;announce_T + aly_peek_T.bob_peek_T.
+echo -- Aly peeks T in the first event and Bob figures it out in the second event.
 define Example9b (Two & Box(Rb,Box(Ra,Cn(World(aly%_peek%_T),Event))));
 echo -- (Two & Box(Rb,Box(Ra,Cn(World(aly_peek_T),Event))))
 regex Example9b;

testkf/epi1-test2.k

@@ -93,7 +93,8 @@ query Example8 = (Two & ~aly(~(bob_peek_H ; _)))
 query Example9a = (Two & ~bob(~~aly(~(bob_peek_T ; _))))
 
 -- 9b. Bob knows that Aly knows that Aly peeked T in the first step
--- The result should be bob_peek_H.announce_H + bob_peek_H.aly_peek_H
+-- The result should be aly_peek_T;announce_T + aly_peek_T.bob_peek_T.
+-- Aly peeks T in the first event and Bob figures it out in the second event.
 -- (Two & ~bob(~~aly(~(aly_peek_T ; _))))
 query Example9b = (Two & ~bob(~~aly(~(aly_peek_T ; _))))
 

testkf/test2.base

@@ -38,7 +38,8 @@ Com(The result should be bob_peek_H.announce_H + bob_peek_H.aly_peek_H)
 Query2(Example9a,And(Two,Boxbob(Boxaly(Con(World(bob_peek_T),Ev)))))
 
 Com(9b. Bob knows that Aly knows that Aly peeked T in the first step)
-Com(The result should be bob_peek_H.announce_H + bob_peek_H.aly_peek_H)
+Com(The result should be aly_peek_T;announce_T + aly_peek_T.bob_peek_T.)
+Com(Aly peeks T in the first event and Bob figures it out in the second event.)
 Query2(Example9b,And(Two,Boxbob(Boxaly(Con(World(aly_peek_T),Ev)))))