[CZT-Users] ZLive eval questions

[Michael L. <leu...@cs...>]

HI,

I have been experimenting with the eval option of ZLive. It is nice to have a REPL where one can type in expressions and predicates.


I have a few questions concerning set comprehensions in Z / Z Live, as I may be doing something wrong.

I started ZLive like this, and many tests worked flawlessly:

$ rlwrap java -jar czt.jar zlive
ZLiveDefault> version
ZLive version 1.6-SNAPSHOT, (C) 2006, Mark Utting


1)
First, there are a few set comprehensions where ZLive complains:

ZLiveDefault> eval \# \{f : (0 \upto 1) \fun (0 \upto 1)| f(0)=0  \}
Undefined!  Mu expression has no solutions: (mu

  tmp38 == 0;                   %% tmp38=tmp37,:0..0,    
  tmp37 = tmp38;                %% tmp37:0..0,    
  %%---------------
  p{1=0} in f :: 0.0 ;          %% p={1=tmp37, 2=tmp39},    
  tmp37 = p.1;
  tmp39 = p.2                   %% tmp39:0..0,    
@ tmp39
)

According to my understanding, the equivalent B expression would be card({f| f:0..1 --> 0..1 & f(0)=1})
which is defined and whose value is 2 (you can try this out here http://stups.hhu.de/ProB/w/ProB_Logic_Calculator).
Am I missing a difference between Z and B ?
I actually assume it is related to the issue 3) below.

2)
Another example I tried was this:
ZLiveDefault> eval \{ x : \power( (0\upto 4) \cross (0\upto 4)) | \#(x)=4 \land \dom x = 1 \upto 4 \land \ran x = \{2\} \}
WARNING: changing x id from 2142 to 2182
WARNING: changing x id from 2142 to 2186
Error: Cannot generate members of SetComp: { x in x :: 1000.0 ;
tmp276 = x.1 @ tmp276 }
while evaluating&printing the result: { tmp267 == 0;                  %% tmp267:0..0,    
...
(The corresponding B expression is according to my understanding:{x|x : POW((0..4)*(0..4)) & card(x)=4 & dom(x)=1..4 & ran(x)={2}} ).


3)
Now are a few examples where I feel the result is wrong.


ZLiveDefault> eval  \{f : (0 \upto 1) \fun (0 \upto 1)| \{0 \mapsto 0\} \subseteq f  \}
\{ \{ ( 0 , 0 ) \} , \{ ( 0 , 0 ) , ( 1 , 0 ) \} , \{ ( 0 , 0 ) , ( 1 , 1 ) \} , \\
 \{ ( 0 , 0 ) , ( 1 , 0 ) , ( 1 , 1 ) \} , \{ ( 0 , 0 ) , ( 0 , 1 ) \} , \\
 \{ ( 0 , 0 ) , ( 0 , 1 ) , ( 1 , 0 ) \} , \{ ( 0 , 0 ) , ( 0 , 1 ) , ( 1 , 1 ) \} , \\
 \{ ( 0 , 0 ) , ( 0 , 1 ) , ( 1 , 0 ) , ( 1 , 1 ) \} \}
ZLiveDefault> eval  \# \{f : (0 \upto 1) \fun (0 \upto 1)| \{0 \mapsto 0\} \subseteq f  \}
8

I tried to re-code the set comprehension slightly differently, but get the same result:

ZLiveDefault> eval  \# \{f : \power((0 \upto 1) \cross (0 \upto 1))| f\in (0\upto 1) \fun (0\upto 1) \land \{0 \mapsto 0\} \subseteq f  \}
8

According to my understanding the equivalent version in B is this:

>>> card({f|f:0..1 --> 0..1 & {0|->0} <: f})
 ⇝  card({f|f ∈ 0 ‥ 1 → 0 ‥ 1 ∧ 0 ↦ 0 ∈ f})
Expression Value = 
2


To me it seems that ZLive is treating \fun, \bij, … all like \rel :

ZLiveDefault> eval  \# \{f : \power((0 \upto 1) \cross (0 \upto 1))| f\in (0\upto 1) \bij (0\upto 1)  \}
16

Indeed, I get:

ZLiveDefault> eval (0\upto 1)\fun (0\upto1)
\power ( \{ 0 , 1 \} \cross \{ 0 , 1 \} )
ZLiveDefault> eval (0\upto 1)\bij (0\upto1)
\power ( \{ 0 , 1 \} \cross \{ 0 , 1 \} )

Kind Regards,
Michael Leuschel