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

[Bernard L. <blo...@te...>]

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:  <mailto:blo...@te...> blo...@te...

Em:  <mailto:blo...@ov...> blo...@ho...

IM: SkypeName:  bernard.londeix

W:  <http://www.telmaco.co.uk/> http://www.telmaco.co.uk

Tw:  <http://www.twitter.com/Telmaco> http://www.twitter.com/Telmaco

Tw:  <http://www.twitter.com/MeterIT> 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 ---------------