Menu
▾
▴
Re: [CZT-Users] CZT - Looking for help with Z Live
|
From: Yves L. <Yve...@im...> - 2012-07-13 18:18:05
|
Dear CZters,
I have tried to answer Bernard's questions, but some problems
remain. Can you please give us some hints on the use of ZLive? Thanks!
Le 12/07/2012 23:11, Bernard Londeix a écrit :
> Dear Yves,
>
> Thank you very much for your kind introduction to ZLive. The NatVar.zed is
> running very well on my machine and this gave me a good idea about what
> should happen.
> I understand this is not your preferred tool but I would like to give a
> chance to ZLive because of the GUI associated with it. It seems to make the
> running tidier than the "Command Prompt" on my MS Windows environment.
> If later I discover that I cannot get what I need out of ZLive I will follow
> your example with Jaza.
>
> To build on the NatVar.zed success I created with Zword a very small case
> with 1 state variable and 4 Schemas. My small case doesn't work even by
> running it the same way as for NatVar.zed.
>
> I note that:
> (i) - I cannot get a file suffix .zed as you do. I am getting a .zed8. Is it
> important?
Actually my .zed file is a file in the latex format. The suffix could
also be .tex.
It seems that .zed8 means that the file is using Unicode markup (which
I don't use). I guess that you should change the markup setting of zlive
by typing something like
set markup UNICODE
before you load your file.
> (ii) - my "do Schema" gives my an error message:
> Error: evaluation too difficult/large: Cannot find mode . . .
I have the same problem with the file door.zed (attached to this file).
I don't understand this error message. Maybe another member of the list
can help us...
> (iii) - a command "set variable value" gives me unknown setting as if my
> variable were not known or defined.
The set <var> <value> only concerns the variables of zlive: markup,
section, givensetsize,... not the variables of your specification.
> (iv) - Other error (When my variable 'door' is very well declared):
> abc01> eval door = close
> term contains type errors
> "StringSource", line 1: Undeclared name: door
>
eval is aimed at evaluating expressions outside the context of
a schema. For example
ZLiveDefault> eval 1+1
2
But eval does not see the variables declared in your schemas. I guess
it is the same for evalp.
If you want to check that your door is closed, you can write a schema
like
\begin{zed}
Boolean ::= Vrai| Faux
\end{zed}
\begin{schema}
\Xi MyDoorSchema
r! : Boolean
\where
(door = close) \implies r! = Vrai\\
(door \neq close) \implies r! = Faux\\
\end{schema}
(see files door.zed and doorJaza.zed in attachment.
I am unable to run door.zed but I get the following results with Jaza:
JAZA> load doorJaza.zed
Loading 'doorJaza.zed' ...
Added 5 definitions.
JAZA> do DoorInit
\lblot door'==close \rblot
JAZA> ; EvalDoor
\lblot door'==close, r!==Vrai \rblot
> Would you know of which steps should I follow to clarify this problem?
>
I hope that some czters will help us do the same in Zlive
Sincerely yours
Yves
PS: I'll be out of office in the coming weeks
> Thanks for the guidance,
>
> Kind regards,
>
> Bernard
>
>
> -----Original Message-----
> From: Yves Ledru [mailto:Yve...@im...]
> Sent: 11 July 2012 11:36
> To: czt...@li...; blo...@te...
> Subject: Re: [CZT-Users] CZT - Looking for help with Z Live
>
> 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
> |______________________________________________________________________
>
>
>
--
___ 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
|______________________________________________________________________
|
