[CZT-Devel] executing ZLive from command line

[Urmas R. <ur...@ho...>]

Hello.

Thanks for previous replies.

At the moment i have simple test specification in test.utf8 file as were suggested:

 ┌AddAB
 a?, b?, c!: ℕ  
 |
 c! = a?+b?  
└

My goal is to execute this specifications from command line without any interactive mode with inputs 1 and 2 from command line and to get output 3.
I am using the ZLive animator, i can load the specification from command line:

java -jar czt.jar zlive --load test.utf8 

loads the specification and proceeds to interactive mode. I need to pass arguments and execute specification from command line avoiding any interactive modes.

java -jar czt.jar zlive --help

Gives me

ZLive version 1.6-SNAPSHOT, (C) 2006, Mark Utting
Options:
  --help         (print this help message)
  --logrules     (print rule-unfolding debug messages into zlive.log)
  --logeval      (print evaluation debug messages into zlive.log)
  --load SPEC    (load the Z specification SPEC)
  --test SECTION (evaluate all conjectures in SECTION)
If there are no --test arguments, ZLive goes into interactive mode,
using the last section of the last SPEC loaded.

I can test any section, this should be AddAB section. But i am not completely sure what the --test command do,  evaluate all conjectures in SECTION, is this means animation?
Or i want to use maybe eval parameter from command line but unfortunately ZLive does not have this option in its argument's list.

If i want to test AddAB i get error message:

java -jar czt.jar zlive --load test.utf8 --test AddAB
ZLive version 1.6-SNAPSHOT, (C) 2006, Mark Utting
Loading section Specification
Exception in thread "main" net.sourceforge.czt.session.SourceLocator$SourceLocatorException: Cannot find source for section AddAB with czt.path=null
    at net.sourceforge.czt.session.Sour
   ................

Maybe somebody can help me with how to use eval command from ZLive parameter's list? Or the --test parameter?
Or maybe the specification should be rewritten in order to have some main executable section in order to be tested without eval?

With best wishes,
Urmas Repinski.







> Date: Thu, 13 Oct 2011 02:30:10 +1300
> From: Pet...@ec...
> To: czt...@li...
> Subject: Re: [CZT-Devel] installing CZT
> 
> Hello Urmas,
> 
> > Is there any tutorial how to animate the specification using CZT?
> 
> I am not really familiar with animation but I hope I can help you to get
> started.  I am not aware of a tutorial but ZLive, the animator, provides
> quite good help messages.  Once you've started ZLive, you can type
> "help" and it will tell you what you can do.
> 
> > For example i have simple specification like
> > 
> > ┌AddAB
> >       a?, b?, c!: ℕ  
> >      |
> >        c! = a?+b?  
> > └
> > 
> > 
> > 
> > I would like to get output 3 if i provide inputs 1 and 2.
> 
> I put your little spec into file test.utf8, then started ZLive and typed:
>   load test.utf8
>   eval AddAB \land [a?, b? : \nat | a? = 1 \land b? = 2]
> As you can see, I used the schema calculus to constrain AddAB to the
> inputs you are interested in.  I don't know whether that's the normal
> way to do it but it seems to work.  The output of ZLive is
>   \{ \lblot a? == 1 , b? == 2 , c! == 3 \rblot \}
> and you can see that c! must be 3.
> 
> > is it possible to animate the specification using command line?
> 
> You can use ZLive as a command line tool by executing:
>   java -jar czt.jar zlive
> 
> > Is it possible to store outputs in output file and read inputs from
> > input file?
> 
> In my example above, I already used input files.
> I don't know whether it is possible to store outputs but have a look at
> the help messages provided and you might find out.
> 
> Hope this helps,
> Petra
> 
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2d-oct
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel