Menu
▾
▴
Re: [CZT-Devel] installing CZT
|
From: Leo F. <leo...@ne...> - 2011-10-12 15:29:46
|
Urmas,
I still don't quite understand what you are trying to animate (e.g., where does your Z spec will come from?),
but the general guideline is that it needs to be concrete enough, and bounded / finite. So "\nat" wouldn't work
well, unless you have fixed values / equations for the variables, like in your example.
So far as I understand it, ZLive's strength is in that it is fully Z-ISO compatible, which means it will process mostly
all Z specs (that are concrete enough) quite naturally. Another strength is that it has a rule-based mechanism where
you can influence the way the rewriting / animation engine works, and that is quite a strength, given it would be
in the direction of semi-automated theorem proving. (Now I am guessing), a weakness might perhaps be in the
reasoning power the tool will have in the presence of complex invariants / predicates. But then it will depend on
the nature of your model.
Another tool that might be suitable for animation is ProZ, although it is not within CZT toolset. The strengths of ProZ
is that it can handle pretty complicated invariants, has integration with sat solvers, state-space graphical visualisation etc
(E.g., it is based in Prolog). The weakeness is that it's just a prototype: although it covers a lot of (Spivey / old) Z, it doesn't
handle the schema calculus as naturally (e.g., it is a tool developed originally for the B method and CSP). Having said
that, it works well for certain kind of Z specs, and I use it when I want to know more about intricate aspects of a model that
I don't understand well (yet).
However, without knowing better what do you want to achieve, it is a bit difficult to see what would be most suitable :-)
By the way, you mentioned this was part of your PhD, could you send us (or me) the PhD proposal / topic, for instance?
Hope this helps....
Best,
Leo
On 12 Oct 2011, at 08:11, Urmas Repinski wrote:
Hello,
I have one more question at the moment if its possible.
Is there any tutorial how to animate the specification using CZT?
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.
is it possible to animate the specification using command line?
Is it possible to store outputs in output file and read inputs from input file?
Can this operations be defined in specification or i have to provide inputs as parameters?
Urmas.
________________________________
From: ur...@ho...<mailto:ur...@ho...>
To: czt...@li...<mailto:czt...@li...>
Date: Tue, 11 Oct 2011 10:51:28 +0200
Subject: [CZT-Devel] installing CZT
Hello,
I had recently downloaded the last fixes, and now the installation comes through.
[INFO] Reactor Summary:
[INFO]
[INFO] Community Z Tools ................................. SUCCESS [1.479s]
[INFO] CZT Util .......................................... SUCCESS [5.354s]
[INFO] CZT Jaxb .......................................... SUCCESS [17.602s]
[INFO] CZT ZML ........................................... SUCCESS [2.448s]
[INFO] CZT GnAST ......................................... SUCCESS [2.387s]
[INFO] CZT GnAST Maven Plugin ............................ SUCCESS [2.791s]
[INFO] CZT Corejava ...................................... SUCCESS [3:22.958s]
[INFO] CZT SpecReader .................................... SUCCESS [4.513s]
[INFO] CZT Session ....................................... SUCCESS [3.272s]
[INFO] CZT Java Cup ...................................... SUCCESS [4.908s]
[INFO] CZT Parser Source ................................. SUCCESS [1.528s]
[INFO] CZT Cup Maven Plugin .............................. SUCCESS [1.329s]
[INFO] CZT Parser ........................................ SUCCESS [1:29.434s]
[INFO] CZT Z Pattern Parser .............................. SUCCESS [20.646s]
[INFO] CZT Typechecker ................................... SUCCESS [25.878s]
[INFO] CZT Rules ......................................... SUCCESS [29.582s]
[INFO] CZT ZLive ......................................... SUCCESS [22.648s]
[INFO] CZT Gaffe ......................................... SUCCESS [11.563s]
[INFO] CZT Gaffe2 ........................................ SUCCESS [4.354s]
[INFO] CZT jEdit plugins ................................. SUCCESS [0.332s]
[INFO] CZT ZLive jEdit Plugin ............................ SUCCESS [1.365s]
[INFO] CZT Object Z Parser ............................... SUCCESS [27.113s]
[INFO] CZT Object-Z Typechecker .......................... SUCCESS [19.771s]
[INFO] CZT Z/Eves (proofs) Parser ........................ SUCCESS [1:30.195s]
[INFO] CZT Z/Eves (proofs) Typechecker ................... SUCCESS [44.580s]
[INFO] CZT Z VCG ......................................... SUCCESS [21.737s]
[INFO] CZT ZSideKick jEdit Plugin ........................ SUCCESS [6.955s]
[INFO] CZT Z Palette jEdit Plugin ........................ SUCCESS [1.407s]
[INFO] CZT Z/Eves Integration ............................ SUCCESS [44.098s]
[INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS [2.165s]
[INFO] CZT Circus Parser ................................. SUCCESS [1:02.805s]
[INFO] CZT Object Z Pattern Parser ....................... SUCCESS [32.151s]
[INFO] CZT Circus Typechecker ............................ SUCCESS [16.917s]
[INFO] CZT User Interface ................................ SUCCESS [30.234s]
[INFO] CZT Z to B translator ............................. SUCCESS [9.747s]
[INFO] ------------------------------------------------------------------------
[INFO] BUILD SUCCESS
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 14:27.724s
[INFO] Finished at: Tue Oct 11 11:44:46 EEST 2011
[INFO] Final Memory: 47M/769M
[INFO] ------------------------------------------------------------------------
So i have jar files generated in lib folder, will try to attach them with c++ command line.
If somebody has any corresponding experience how to execute CZT from c++ then please let me know to make things simpler.
Thank You,
Urmas.
------------------------------------------------------------------------------ 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...<mailto:CZT...@li...> https://lists.sourceforge.net/lists/listinfo/czt-devel
<ATT00001..txt><ATT00002..txt>
|
