Re: [CZT-Users] CZT - Looking for help with Z Live

[Yves L. <Yve...@im...>]

Dear Bernard,

I am not so much used to CZT/ZLive. I use Jaza (the ancestor of ZLive).
http://www.cs.waikato.ac.nz/~marku/jaza/

At this point, it seems that Jaza still covers a larger subset of Z than
ZLive.

But I can try to help you to get started with ZLive.
To illustrate the use of ZLive I'll use
a simple specification of a natural variable which can be
incremented, decremented,... (see attached file).
Here are the first commands to issue.

First you call ZLive:

java -jar czt.jar zlive

then it is good practice to do "reset"

ZLiveDefault> reset
All specifications cleared...

Now you load your specification

ZLiveDefault> load NatVar.zed
Loading section NatVar
Setting section to NatVar

Use the "do" command to start an animation. Here I start it by calling 
the init operation

NatVar> do XVarInit
(I skip the warning messages)
1: \lblot x == 0 , x' == 0 \rblot

It answers by giving the assignment of all schema variables (here
x and x').

You can then start from this resulting state to call an operation. This
is done by using ";" followed by the name of the schema. Let us 
increment x...

NatVar> ; XVarInc
1: \lblot x == 0 , x' == 1 \rblot

Let us do it a second time

NatVar> ; XVarInc
1: \lblot x == 1 , x' == 2 \rblot


I add some difficulties to call an operation with input and output 
parameters (in Jaza you simply call ; XVarAdd [i? := 5]) ,
finally, I found the following solution based on schema conjunction
(maybe ZLive experts can point to a simpler way to assign values to
input parameters):

NatVar> ; XVarAdd \land [i? : \num \where i? = 5]
1: \lblot x == 2 , x' == 7 , i? == 5 , r! == 7 \rblot

Finally to close these examples, let us restart from the init
state and try to decrement natural variable x

NatVar> do XVarInit
1: \lblot x == 0 , x' == 0 \rblot
NatVar> ; XVarDec
no more solutions

Which says that it does not find solutions (because x may not
take negative values).

I hope this helps getting started with ZLive. (you might want
to do the same with Jaza, but for Jaza you need to change
the init operation as follows:

\begin{schema}{XVarInit}
\Delta XVar
\where
x' = 0
\end{schema}

Sincerely yours

Yves

Le 09/07/2012 23:36, Bernard Londeix a écrit :
> Dear Sir,
>
> I am trying to animate a very small Z specification which is type
> checked correctly with Z Word.
>
> Unfortunately I am getting nowhere with Z Live. This is probably due to
> my not understanding correctly the Help. See below:
>
> Would you have a user guide for real beginners?
>
> What are the 3 or 4 first commands to issue to CZT Live in order to
> Animate a small specification?
>
> Thanks,
>
> Best regards,
>
> *Bernard Londeix*
>
> ---------------------------------------------------------------------------
>
> *Telmaco Ltd*
>
> *M: +44 7768 588 419*
>
> *E: blo...@te... <mailto:blo...@te...>*
>
> *Em: blo...@ho... <mailto:blo...@ov...>*
>
> *IM: SkypeName:  bernard.londeix*
>
> *W: http://www.telmaco.co.uk <http://www.telmaco.co.uk/>*
>
> *Tw: http://www.twitter.com/Telmaco*
>
> *Tw: http://www.twitter.com/MeterIT*
>
> ---------------------------------------------------------------------------
>
> **
>
> --------------- ZLive Commands ---------------
>
> load file.tex     -- Read a Z specification into ZLive
>
> eval <expr>       -- Evaluate an expression
>
> evalp <pred>      -- Evaluate a predicate (synonym for eval)
>
> do <expr>         -- Evaluate a schema/set and show one member
>
> next/curr/prev    -- Show next/current/previous state of a schema/set
>
> ; schemaExpr      -- Compose the current state with schemaExpr
>
> undo              -- Undo the last 'do' or ';' command.
>
> why               -- Show the internal code of the last do or ';' command
>
> set               -- Show all current settings
>
> set <var> <value> -- Sets <var> to <value>.
>
> show              -- Show name & type of defns in current section
>
> conjectures       -- Evaluate all conjectures in the current section
>
> reset             -- Remove all loaded specifications
>
> version           -- Display the version of ZLive
>
> help              -- Display this help summary
>
> quit              -- Exit the ZLive program
>
>    env             -- Show internal defn/operator tables
>
>    unfold term     -- Show term after initial unfolding (debug)
>
>    apply rule expr -- Try to rewrite expr using rule (debug)
>
> --------------- End of ZLive Commands ---------------
>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
>
>
>
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users
>


-- 
  ___ Yves LEDRU _______________________________________________________
| Professeur à l'Université Joseph Fourier (Grenoble-1)
| LIG, Domaine Universitaire, BP 72,         Tel: + 33 4 76 82 72 16
| F-38402 St Martin D'Heres Cedex            e-mail: Yve...@im...
| FRANCE                http://www-lsr.imag.fr/Les.Personnes/Yves.Ledru
|______________________________________________________________________