czt-devel — For programmers using the CZT code

[CZT-Devel] more on memory improvements

[Leo F. <leo...@ne...>]

Hi,

I've been running more profiling sessions on larger examples (e.g., complete mondex and xenon), which requires about 400-800MB of raw memory to run.
Interestingly, running the VCG through mondex completely would crash the Eclipse environment (e.g., with 4-8GB maximum Java heap).
Now it runs much more smoothly and it takes just a few seconds within the Eclipse environment - and quite quickly both on the command line and under the profiler. 

Bits that I am still puzzled about is the presence of various (list and normal) iterators in the "live" memory (see the snapshot attached).

Still investigating....

Re: [CZT-Devel] Memory allocation with ArrayLists; arrays; etc.

[Tim M. <tm...@un...>]

Nice work!

When you say you added "parser = null", I assume you mean after you do 
the parsing? This would mean that, prior to your change, a reference to 
the parser is being kept even after the variable scope of the variable 
"parser" ends? That seems odd.

On 25/01/12 01:22, Leo Freitas wrote:
> Tim,
>
> I've forgot to mention below that I was talking about parsing and typechecking only.
>
> I've just run the same profiling setup on the VCG for these larger examples and yes, the worst ones were
> Object[] (24%), char[] (17.3%), ArrayList[] (9%) and BigInteger (2-3%).
>
> Surprising ones were int[] (6.5%) and short[] (6%) arrays, since they are not explicitly created anywhere in CZT.
> LocalAnn took 3%; Iterators were also a surprise: both iterator() and listIterator() cover about 10%, where more
> obvious ones like String (0.9%) and ZName (1.7%) were quite low.
>
> I've run the profiling sessions about 3-5 times on each example taking the average.
>
> ----
>
> Searching for potential sources of such unexpected types, I managed to find a few successful candidates:
>
> a) ParseUtils
>
> char[], short[], and int[] are mostly present in the Java CUP low-level classes to represent the internal parsing tables from the grammar.
> I simply added an explicit "parser = null" to the main ParseUtils.parse method. These arrays combined account for about 30% of memory.
>
> after the change, these arrays now account for 1.1% (!!!) that's quite an improvement.
>
> b) ListIterator and Iterator
>
> These appear in various places, but places that should influence all runs are only on SmartScanner (and possibly PrettyPrinter).
> After this change, they went from a combined (ListIterator + Iterator) 49% footprint to 17%; another good improvement.
>
> d) ArrayList and Object[]
>
> There are various places and identifying where are the ones of most significance is tedious/time-consuming.
> Instead, I've done a thorough search through various projects and changed default constructors to more sensible values, when possible,
> or to a parameterised default when not (e.g., PerformanceSettings interface in util project).
>
> This led to a decrease in the memory footprint of these objects of....
>
> e) BigInteger
>
> Why do we need big integers within LocAnn and other places? I guess because long would be potentially small?
> But would there really be something bigger than 2^32 or 2^64 in number of lines of source in a file say? Hum...
>
> In terms of memory footprint, it varied between 0.7% to 3%, depending on the example. I won't change this one for now.
>
> f) Garbage collection time
>
> Firstly it was about 16-20% now it was about 46.1% of time taken. Don't know if that's related to changes, but looks like it.
>
> ======
>
> Changes a) and b) led to a drastic memory footprint decrease from 8MB to 0.91MB;
> Other changes led to a minor improvement in comparison (i.e., 0.80MB).
>
> That's despite the fact that changes in d) were the most numerous - they didn't amount to much improvement, but some.
>
> Hopefully this will enable much better performance on larger specs. I am committing it now to see how it goes.
>
> Best,
> Leo
>
> On 23 Jan 2012, at 14:00, Leo Freitas wrote:
>
>> Hi Tim,
>>
>> That's interesting. I';ve been doing similar (profiling) tests over specs of some size (e.g., Mondex, Tokeneer, Xenon, IEEE float point unit);
>> although I guess they are smaller than iFACTS - apart from Xenon, which is quite large.
>>
>> On the profiling sessions, the worst culprit was "char[]" arrays, mostly from the java_cup lexer. The Object[] and ArrayList[] were about 2-3% each,
>> for what the char[] was 90% (!)... Similarly, on profiling CPU, it was the IO operations on zzRefill within the java_cup scanner that took the largest chunk
>> of the time (27%). Smart scanning (e.g., lookahead) has taken only about 2-3%.
>>
>> I wonder... what was the profilling setup that you used to get to the creation of Object[] ArrayList as the main problem?
>> Although the change you refer to below shouldn't be relatively simple to change, as Petra pointed out.
>>
>> I just want to get the right picture to tackle such performance problem for larger specs.
>>
>> Best,
>> Leo
>>
>> On 5 Jan 2012, at 23:51, Tim Miller wrote:
>>
>>> Hi everyone,
>>>
>>> Anthony Hall and I have been discussing some memory problems that CZT
>>> has when parsing large specifications. Anthony has been trying to
>>> typecheck the iFacts specification, but without much luck due to the
>>> large memory resources.
>>>
>>> We've each been playing around with VisualVM, and Anthony pointed out is
>>> that the two largest memory hogs are Object[] and ArrayList, taking up
>>> around 23% and 10% of the heap respectively.
>>> Most of the object arrays and ArrayLists contain exactly 10 items, and
>>> almost all items in these lists are null.
>>>
>>> After some poking around, I discovered that when ArrayList is created
>>> using the default constructor, it allocates 10 items initially. This
>>> appears to be where the 10 items come from in each case. I suspect this
>>> may also be contributing to some of the memory problems, considering
>>> that CZT has so many empty annotation lists, etc. Creating ArrayLists
>>> with an initial capacity of 0 or 1 (using the constructor ArrayList(int
>>> initialCapacity)) may give us some substantial space savings
>>>
>>> It appears that most ArrayLists are created in the gnast-generated code.
>>> Petra, how difficult would it be to create these lists using this other
>>> constructor?
>>>
>>> Regards,
>>> Tim
>>>
>>> ------------------------------------------------------------------------------
>>> Ridiculously easy VDI. With Citrix VDI-in-a-Box, you don't need a complex
>>> infrastructure or vast IT resources to deliver seamless, secure access to
>>> virtual desktops. With this all-in-one solution, easily deploy virtual
>>> desktops for less than the cost of PCs and save 60% on VDI infrastructure
>>> costs. Try it free! http://p.sf.net/sfu/Citrix-VDIinabox
>>> _______________________________________________
>>> CZT-Devel mailing list
>>> CZT...@li...
>>> https://lists.sourceforge.net/lists/listinfo/czt-devel
>>
>>
>> ------------------------------------------------------------------------------
>> Try before you buy = See our experts in action!
>> The most comprehensive online learning library for Microsoft developers
>> is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
>> Metro Style Apps, more. Free future releases when you subscribe now!
>> http://p.sf.net/sfu/learndevnow-dev2
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
>
>

Re: [CZT-Devel] Memory allocation with ArrayLists; arrays; etc.

[Leo F. <leo...@ne...>]

Tim,

I've forgot to mention below that I was talking about parsing and typechecking only.

I've just run the same profiling setup on the VCG for these larger examples and yes, the worst ones were 
Object[] (24%), char[] (17.3%), ArrayList[] (9%) and BigInteger (2-3%). 

Surprising ones were int[] (6.5%) and short[] (6%) arrays, since they are not explicitly created anywhere in CZT.
LocalAnn took 3%; Iterators were also a surprise: both iterator() and listIterator() cover about 10%, where more
obvious ones like String (0.9%) and ZName (1.7%) were quite low. 

I've run the profiling sessions about 3-5 times on each example taking the average.

----

Searching for potential sources of such unexpected types, I managed to find a few successful candidates:

a) ParseUtils

char[], short[], and int[] are mostly present in the Java CUP low-level classes to represent the internal parsing tables from the grammar.
I simply added an explicit "parser = null" to the main ParseUtils.parse method. These arrays combined account for about 30% of memory.

after the change, these arrays now account for 1.1% (!!!) that's quite an improvement. 

b) ListIterator and Iterator

These appear in various places, but places that should influence all runs are only on SmartScanner (and possibly PrettyPrinter).
After this change, they went from a combined (ListIterator + Iterator) 49% footprint to 17%; another good improvement.

d) ArrayList and Object[]

There are various places and identifying where are the ones of most significance is tedious/time-consuming. 
Instead, I've done a thorough search through various projects and changed default constructors to more sensible values, when possible,
or to a parameterised default when not (e.g., PerformanceSettings interface in util project). 

This led to a decrease in the memory footprint of these objects of....

e) BigInteger

Why do we need big integers within LocAnn and other places? I guess because long would be potentially small? 
But would there really be something bigger than 2^32 or 2^64 in number of lines of source in a file say? Hum...

In terms of memory footprint, it varied between 0.7% to 3%, depending on the example. I won't change this one for now.

f) Garbage collection time

Firstly it was about 16-20% now it was about 46.1% of time taken. Don't know if that's related to changes, but looks like it.

======

Changes a) and b) led to a drastic memory footprint decrease from 8MB to 0.91MB;
Other changes led to a minor improvement in comparison (i.e., 0.80MB).

That's despite the fact that changes in d) were the most numerous - they didn't amount to much improvement, but some.

Hopefully this will enable much better performance on larger specs. I am committing it now to see how it goes.

Best,
Leo

On 23 Jan 2012, at 14:00, Leo Freitas wrote:

> Hi Tim,
> 
> That's interesting. I';ve been doing similar (profiling) tests over specs of some size (e.g., Mondex, Tokeneer, Xenon, IEEE float point unit); 
> although I guess they are smaller than iFACTS - apart from Xenon, which is quite large.
> 
> On the profiling sessions, the worst culprit was "char[]" arrays, mostly from the java_cup lexer. The Object[] and ArrayList[] were about 2-3% each,
> for what the char[] was 90% (!)... Similarly, on profiling CPU, it was the IO operations on zzRefill within the java_cup scanner that took the largest chunk
> of the time (27%). Smart scanning (e.g., lookahead) has taken only about 2-3%. 
> 
> I wonder... what was the profilling setup that you used to get to the creation of Object[] ArrayList as the main problem?
> Although the change you refer to below shouldn't be relatively simple to change, as Petra pointed out. 
> 
> I just want to get the right picture to tackle such performance problem for larger specs.
> 
> Best,
> Leo
> 
> On 5 Jan 2012, at 23:51, Tim Miller wrote:
> 
>> Hi everyone,
>> 
>> Anthony Hall and I have been discussing some memory problems that CZT 
>> has when parsing large specifications. Anthony has been trying to 
>> typecheck the iFacts specification, but without much luck due to the 
>> large memory resources.
>> 
>> We've each been playing around with VisualVM, and Anthony pointed out is 
>> that the two largest memory hogs are Object[] and ArrayList, taking up 
>> around 23% and 10% of the heap respectively.
>> Most of the object arrays and ArrayLists contain exactly 10 items, and 
>> almost all items in these lists are null.
>> 
>> After some poking around, I discovered that when ArrayList is created 
>> using the default constructor, it allocates 10 items initially. This 
>> appears to be where the 10 items come from in each case. I suspect this 
>> may also be contributing to some of the memory problems, considering 
>> that CZT has so many empty annotation lists, etc. Creating ArrayLists 
>> with an initial capacity of 0 or 1 (using the constructor ArrayList(int 
>> initialCapacity)) may give us some substantial space savings
>> 
>> It appears that most ArrayLists are created in the gnast-generated code. 
>> Petra, how difficult would it be to create these lists using this other 
>> constructor?
>> 
>> Regards,
>> Tim
>> 
>> ------------------------------------------------------------------------------
>> Ridiculously easy VDI. With Citrix VDI-in-a-Box, you don't need a complex
>> infrastructure or vast IT resources to deliver seamless, secure access to
>> virtual desktops. With this all-in-one solution, easily deploy virtual 
>> desktops for less than the cost of PCs and save 60% on VDI infrastructure 
>> costs. Try it free! http://p.sf.net/sfu/Citrix-VDIinabox
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
> 
> 
> ------------------------------------------------------------------------------
> Try before you buy = See our experts in action!
> The most comprehensive online learning library for Microsoft developers
> is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
> Metro Style Apps, more. Free future releases when you subscribe now!
> http://p.sf.net/sfu/learndevnow-dev2
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] Memory allocation with ArrayLists

[Leo F. <leo...@ne...>]

Hi Tim,

That's interesting. I';ve been doing similar (profiling) tests over specs of some size (e.g., Mondex, Tokeneer, Xenon, IEEE float point unit); 
although I guess they are smaller than iFACTS - apart from Xenon, which is quite large.

On the profiling sessions, the worst culprit was "char[]" arrays, mostly from the java_cup lexer. The Object[] and ArrayList[] were about 2-3% each,
for what the char[] was 90% (!)... Similarly, on profiling CPU, it was the IO operations on zzRefill within the java_cup scanner that took the largest chunk
of the time (27%). Smart scanning (e.g., lookahead) has taken only about 2-3%. 

I wonder... what was the profilling setup that you used to get to the creation of Object[] ArrayList as the main problem?
Although the change you refer to below shouldn't be relatively simple to change, as Petra pointed out. 

I just want to get the right picture to tackle such performance problem for larger specs.

Best,
Leo

On 5 Jan 2012, at 23:51, Tim Miller wrote:

> Hi everyone,
> 
> Anthony Hall and I have been discussing some memory problems that CZT 
> has when parsing large specifications. Anthony has been trying to 
> typecheck the iFacts specification, but without much luck due to the 
> large memory resources.
> 
> We've each been playing around with VisualVM, and Anthony pointed out is 
> that the two largest memory hogs are Object[] and ArrayList, taking up 
> around 23% and 10% of the heap respectively.
> Most of the object arrays and ArrayLists contain exactly 10 items, and 
> almost all items in these lists are null.
> 
> After some poking around, I discovered that when ArrayList is created 
> using the default constructor, it allocates 10 items initially. This 
> appears to be where the 10 items come from in each case. I suspect this 
> may also be contributing to some of the memory problems, considering 
> that CZT has so many empty annotation lists, etc. Creating ArrayLists 
> with an initial capacity of 0 or 1 (using the constructor ArrayList(int 
> initialCapacity)) may give us some substantial space savings
> 
> It appears that most ArrayLists are created in the gnast-generated code. 
> Petra, how difficult would it be to create these lists using this other 
> constructor?
> 
> Regards,
> Tim
> 
> ------------------------------------------------------------------------------
> Ridiculously easy VDI. With Citrix VDI-in-a-Box, you don't need a complex
> infrastructure or vast IT resources to deliver seamless, secure access to
> virtual desktops. With this all-in-one solution, easily deploy virtual 
> desktops for less than the cost of PCs and save 60% on VDI infrastructure 
> costs. Try it free! http://p.sf.net/sfu/Citrix-VDIinabox
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] cycles in section parents: parsing or typing error?

[Leo F. <leo...@ne...>]

Hi guys,

Many thanks for this. Our implementation is already in line with this, so will commit soon.

One technicality though: because LatexMarkupFunction is calculated earlier (e.g., as a lexer),
and teh information tables (e.g., optable, joker, thm, proofs, definition, etc) occur later on unicode
stream, and we want a solution that is markup independent, the treatment in the parser is to some
extent repeated for these two parts of the process - I don't think there is any performance penalty
for this (e.g., the process is already quite like that anyway - LMF first; tables later).

Best,
Leo


On 17 Jan 2012, at 21:38, Tim Miller wrote:

> It definitely belongs in the typechecker. There is a note in the 
> "inheriting section" section of the Z standard that says:
> 
> "NOTE 1 Ancestors need not be immediate parents, and a section cannot be 
> amongst its own ancestors (no cycles in the parent relation)."
> 
> It is not part of the type rule though, so I must have missed it when I 
> implemented the type rules.
> 
> Cheers,
> Tim
> 
> On 18/01/12 07:06, Mark Utting wrote:
>> Leo
>> 
>> Doing it in the typechecker sounds best to me.
>> 
>> 1. You might be able to give better error messages there.
>> 2. It will/should work on unicode input, not just latex input.
>> 
>> Cheers
>> Mark
>> 
>> On 18 January 2012 02:07, Leo Freitas <leo...@ne...
>> <mailto:leo...@ne...>> wrote:
>> 
>>    Hi,
>> 
>>    We are trying to solve the problem (e.g., stack overflow) involving
>>    cyclic parents of sections.
>>    The error occurs when calculating the latex markup function of
>>    parents during parsing.
>> 
>>    Our change/solution avoids the error, and enables sections with
>>    cyclic parents to be parsed.
>>    Next, the typechecker ensures that the cycle is an error (e.g., note
>>    1, p. 5, 13.2.2.1).
>> 
>>    So the question is, should the error be flagged by the parser or the
>>    typechecker?
>>    Looking at the standard, this we couldn't find where it would be. At
>>    the moment,
>>    we have it at the typechecker.
>> 
>>    Comments?
>> 
>>    Leo & Andrius
>>    ------------------------------------------------------------------------------
>>    Keep Your Developer Skills Current with LearnDevNow!
>>    The most comprehensive online learning library for Microsoft developers
>>    is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
>>    Metro Style Apps, more. Free future releases when you subscribe now!
>>    http://p.sf.net/sfu/learndevnow-d2d
>>    _______________________________________________
>>    CZT-Devel mailing list
>>    CZT...@li... <mailto:CZT...@li...>
>>    https://lists.sourceforge.net/lists/listinfo/czt-devel
>> 
>> 
>> 
>> 
>> ------------------------------------------------------------------------------
>> Keep Your Developer Skills Current with LearnDevNow!
>> The most comprehensive online learning library for Microsoft developers
>> is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
>> Metro Style Apps, more. Free future releases when you subscribe now!
>> http://p.sf.net/sfu/learndevnow-d2d
>> 
>> 
>> 
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
> 
> 
> ------------------------------------------------------------------------------
> Keep Your Developer Skills Current with LearnDevNow!
> The most comprehensive online learning library for Microsoft developers
> is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
> Metro Style Apps, more. Free future releases when you subscribe now!
> http://p.sf.net/sfu/learndevnow-d2d
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] cycles in section parents: parsing or typing error?

[Tim M. <tm...@un...>]

It definitely belongs in the typechecker. There is a note in the 
"inheriting section" section of the Z standard that says:

"NOTE 1 Ancestors need not be immediate parents, and a section cannot be 
amongst its own ancestors (no cycles in the parent relation)."

It is not part of the type rule though, so I must have missed it when I 
implemented the type rules.

Cheers,
Tim

On 18/01/12 07:06, Mark Utting wrote:
> Leo
>
> Doing it in the typechecker sounds best to me.
>
> 1. You might be able to give better error messages there.
> 2. It will/should work on unicode input, not just latex input.
>
> Cheers
> Mark
>
> On 18 January 2012 02:07, Leo Freitas <leo...@ne...
> <mailto:leo...@ne...>> wrote:
>
>     Hi,
>
>     We are trying to solve the problem (e.g., stack overflow) involving
>     cyclic parents of sections.
>     The error occurs when calculating the latex markup function of
>     parents during parsing.
>
>     Our change/solution avoids the error, and enables sections with
>     cyclic parents to be parsed.
>     Next, the typechecker ensures that the cycle is an error (e.g., note
>     1, p. 5, 13.2.2.1).
>
>     So the question is, should the error be flagged by the parser or the
>     typechecker?
>     Looking at the standard, this we couldn't find where it would be. At
>     the moment,
>     we have it at the typechecker.
>
>     Comments?
>
>     Leo & Andrius
>     ------------------------------------------------------------------------------
>     Keep Your Developer Skills Current with LearnDevNow!
>     The most comprehensive online learning library for Microsoft developers
>     is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
>     Metro Style Apps, more. Free future releases when you subscribe now!
>     http://p.sf.net/sfu/learndevnow-d2d
>     _______________________________________________
>     CZT-Devel mailing list
>     CZT...@li... <mailto:CZT...@li...>
>     https://lists.sourceforge.net/lists/listinfo/czt-devel
>
>
>
>
> ------------------------------------------------------------------------------
> Keep Your Developer Skills Current with LearnDevNow!
> The most comprehensive online learning library for Microsoft developers
> is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
> Metro Style Apps, more. Free future releases when you subscribe now!
> http://p.sf.net/sfu/learndevnow-d2d
>
>
>
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] cycles in section parents: parsing or typing error?

[Mark U. <ma...@cs...>]

Leo

Doing it in the typechecker sounds best to me.

1. You might be able to give better error messages there.
2. It will/should work on unicode input, not just latex input.

Cheers
Mark

On 18 January 2012 02:07, Leo Freitas <leo...@ne...> wrote:

> Hi,
>
> We are trying to solve the problem (e.g., stack overflow) involving cyclic
> parents of sections.
> The error occurs when calculating the latex markup function of parents
> during parsing.
>
> Our change/solution avoids the error, and enables sections with cyclic
> parents to be parsed.
> Next, the typechecker ensures that the cycle is an error (e.g., note 1, p.
> 5, 13.2.2.1).
>
> So the question is, should the error be flagged by the parser or the
> typechecker?
> Looking at the standard, this we couldn't find where it would be. At the
> moment,
> we have it at the typechecker.
>
> Comments?
>
> Leo & Andrius
>
> ------------------------------------------------------------------------------
> Keep Your Developer Skills Current with LearnDevNow!
> The most comprehensive online learning library for Microsoft developers
> is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
> Metro Style Apps, more. Free future releases when you subscribe now!
> http://p.sf.net/sfu/learndevnow-d2d
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>

[CZT-Devel] cycles in section parents: parsing or typing error?

[Leo F. <leo...@ne...>]

Hi,

We are trying to solve the problem (e.g., stack overflow) involving cyclic parents of sections.
The error occurs when calculating the latex markup function of parents during parsing.

Our change/solution avoids the error, and enables sections with cyclic parents to be parsed.
Next, the typechecker ensures that the cycle is an error (e.g., note 1, p. 5, 13.2.2.1). 

So the question is, should the error be flagged by the parser or the typechecker? 
Looking at the standard, this we couldn't find where it would be. At the moment,
we have it at the typechecker.

Comments?

Leo & Andrius

Re: [CZT-Devel] Memory allocation with ArrayLists

[<Pet...@ec...>]

Hi Tim,

You wrote:
> It appears that most ArrayLists are created in the gnast-generated code. 
> Petra, how difficult would it be to create these lists using this other 
> constructor?

It should be straightforward.  The Java templates for the generated
classes are in directory gnast/src/vm and you could just replace all
occurrences of the default ArrayList constructor with the one you proposed.

Changing the base class of most AST classes
util/src/main/java/net/sourceforge/czt/base/impl/TermImpl.java
might have a big influence on its own.

Hope this helps,
Petra

[CZT-Devel] Memory allocation with ArrayLists

[Tim M. <tm...@un...>]

Hi everyone,

Anthony Hall and I have been discussing some memory problems that CZT 
has when parsing large specifications. Anthony has been trying to 
typecheck the iFacts specification, but without much luck due to the 
large memory resources.

We've each been playing around with VisualVM, and Anthony pointed out is 
that the two largest memory hogs are Object[] and ArrayList, taking up 
around 23% and 10% of the heap respectively.
Most of the object arrays and ArrayLists contain exactly 10 items, and 
almost all items in these lists are null.

After some poking around, I discovered that when ArrayList is created 
using the default constructor, it allocates 10 items initially. This 
appears to be where the 10 items come from in each case. I suspect this 
may also be contributing to some of the memory problems, considering 
that CZT has so many empty annotation lists, etc. Creating ArrayLists 
with an initial capacity of 0 or 1 (using the constructor ArrayList(int 
initialCapacity)) may give us some substantial space savings

It appears that most ArrayLists are created in the gnast-generated code. 
Petra, how difficult would it be to create these lists using this other 
constructor?

Regards,
Tim

Re: [CZT-Devel] Z Std extension - schema tagging

[Leo F. <leo...@ne...>]

Hi Mark,

Yes, that's a good idea - and is similar to what ProB/Z does. But it has some shortcomings,
mostly when you have complex state (e.g., using the schema calculus) or promotion...
In the end, I've added those syntactic tags....

PS:
sorry for the delay, I am on holiday :-)

best,
Leo

________________________________________
From: bm....@gm... [bm....@gm...] On Behalf Of Mark Utting [ma...@cs...]
Sent: 10 December 2011 03:19
To: Leo Freitas
Cc: czt...@li...
Subject: Re: [CZT-Devel] Z Std extension - schema tagging

Leo,

Another option might be to specify these things *within* Z.
Then you wouldn't need to extend the language or parser
and other tools wouldn't barf on your extended input.

Eg.  look for a schema with a special name, and use it
fields to specify the structure of the state machine:

\begin{schema}{MachineDefinition}
state:  BirthdayBook
init: InitBirthday
% all other names / fields are public operations
add: RobustAddBirthday
find: RobustFindBirthday
remind: RobustRemind
\end{schema}


???

Cheers
Mark


On 22 August 2011 23:09, Leo Freitas <leo...@ne...<mailto:leo...@ne...>> wrote:
Hi,

I am integrating the Z VCG into the CZT Eclipse plugin. Whilst doing that for refinement (and compact version of precondition) proofs,
I came across the need to know what schema is to be considered as the "State" (+ retrieve, init, concrete, etc).
In other tools, this can be made explicit by the user, yet each time the tool is run. I was thinking about some persistent version using
specific keywords/tags near SchBox AxPara (e.g., "\begin{schema}{S}"). What do you think?

I've implemented this already within the ZEves Z parser and thought to put it into the Z one (haven't committed either).
The "keywords" are treated by the scanner/parser outside of boxes. An example would be something like

======================================================
\begin{zsection}
  \SECTION zstate\_toolkit \parents standard\_toolkit
\end{zsection}

Synonymns for when only (abstract/concrete) state is present?
%%Zword \zstate zstate
%%Zword \zstinit zstinit

%%Zword \zastate zastate
%%Zword \zastinit zastinit
%%Zword \zcstate zcstate
%%Zword \zcstinit zcstinit
%%Zword \zretrieve zretrieve
======================================================
\begin{zsection}
  \SECTION zstatev1 \parents zstate\_toolkit
\end{zsection}

\zstate
\begin{schema}{S}
  x: \nat
\where
  bar > x
\end{schema}

\zstinit
\begin{schema}{SInit}
  S~'
\where
  x' = 0
\end{schema}

======================================================
\begin{zsection}
  \SECTION zstatev2 \parents zstate\_toolkit
\end{zsection}

\zastate
\begin{schema}{AState}
  x: \power \nat
\where
 x \neq \emptyset
\end{schema}

\zastinit
\begin{schema}{ASInit}
  AState~'
\where
  x' = \{ 0 \}
\end{schema}

\zcstate
\begin{schema}{CState}
 y: \seq \nat
\where
  y \neq \langle \rangle
\end{schema}

\zcstinit
\begin{schema}{CStInit}
  CState~'
\where
 y' = \langle 0 \rangle
\end{schema}

\zretrieve
\begin{schema}{Retr}
  AState \\
  CState
\where
  \ran~y = x
\end{schema}

======================================================

If there are no objections, I will keep it to the Z parser. Only if you import zstate_toolkit as a parent
would it "work". So, like fuzz_toolkit and named theorems, I see this as a CZT Z extension....

I've extended the printer and typechecker as well to cope with the new markup and to ensure
there are no duplication (e.g., duplicated state tags).

Comments  / thoughts?

Best,
Leo
------------------------------------------------------------------------------
uberSVN's rich system and user administration capabilities and model
configuration take the hassle out of deploying and managing Subversion and
the tools developers use with it. Learn more about uberSVN and get a free
download at:  http://p.sf.net/sfu/wandisco-dev2dev
_______________________________________________
CZT-Devel mailing list
CZT...@li...<mailto:CZT...@li...>
https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] Z Std extension - schema tagging

[Mark U. <ma...@cs...>]

Leo,

Another option might be to specify these things *within* Z.
Then you wouldn't need to extend the language or parser
and other tools wouldn't barf on your extended input.

Eg.  look for a schema with a special name, and use it
fields to specify the structure of the state machine:

\begin{schema}{MachineDefinition}
state:  BirthdayBook
init: InitBirthday
% all other names / fields are public operations
add: RobustAddBirthday
find: RobustFindBirthday
remind: RobustRemind
\end{schema}


???

Cheers
Mark


On 22 August 2011 23:09, Leo Freitas <leo...@ne...> wrote:

> Hi,
>
> I am integrating the Z VCG into the CZT Eclipse plugin. Whilst doing that
> for refinement (and compact version of precondition) proofs,
> I came across the need to know what schema is to be considered as the
> "State" (+ retrieve, init, concrete, etc).
> In other tools, this can be made explicit by the user, yet each time the
> tool is run. I was thinking about some persistent version using
> specific keywords/tags near SchBox AxPara (e.g., "\begin{schema}{S}").
> What do you think?
>
> I've implemented this already within the ZEves Z parser and thought to put
> it into the Z one (haven't committed either).
> The "keywords" are treated by the scanner/parser outside of boxes. An
> example would be something like
>
> ======================================================
> \begin{zsection}
>   \SECTION zstate\_toolkit \parents standard\_toolkit
> \end{zsection}
>
> Synonymns for when only (abstract/concrete) state is present?
> %%Zword \zstate zstate
> %%Zword \zstinit zstinit
>
> %%Zword \zastate zastate
> %%Zword \zastinit zastinit
> %%Zword \zcstate zcstate
> %%Zword \zcstinit zcstinit
> %%Zword \zretrieve zretrieve
> ======================================================
> \begin{zsection}
>   \SECTION zstatev1 \parents zstate\_toolkit
> \end{zsection}
>
> \zstate
> \begin{schema}{S}
>   x: \nat
> \where
>   bar > x
> \end{schema}
>
> \zstinit
> \begin{schema}{SInit}
>   S~'
> \where
>   x' = 0
> \end{schema}
>
> ======================================================
> \begin{zsection}
>   \SECTION zstatev2 \parents zstate\_toolkit
> \end{zsection}
>
> \zastate
> \begin{schema}{AState}
>   x: \power \nat
> \where
>  x \neq \emptyset
> \end{schema}
>
> \zastinit
> \begin{schema}{ASInit}
>   AState~'
> \where
>   x' = \{ 0 \}
> \end{schema}
>
> \zcstate
> \begin{schema}{CState}
>  y: \seq \nat
> \where
>   y \neq \langle \rangle
> \end{schema}
>
> \zcstinit
> \begin{schema}{CStInit}
>   CState~'
> \where
>  y' = \langle 0 \rangle
> \end{schema}
>
> \zretrieve
> \begin{schema}{Retr}
>   AState \\
>   CState
> \where
>   \ran~y = x
> \end{schema}
>
> ======================================================
>
> If there are no objections, I will keep it to the Z parser. Only if you
> import zstate_toolkit as a parent
> would it "work". So, like fuzz_toolkit and named theorems, I see this as a
> CZT Z extension....
>
> I've extended the printer and typechecker as well to cope with the new
> markup and to ensure
> there are no duplication (e.g., duplicated state tags).
>
> Comments  / thoughts?
>
> Best,
> Leo
>
> ------------------------------------------------------------------------------
> uberSVN's rich system and user administration capabilities and model
> configuration take the hassle out of deploying and managing Subversion and
> the tools developers use with it. Learn more about uberSVN and get a free
> download at:  http://p.sf.net/sfu/wandisco-dev2dev
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>

Re: [CZT-Devel] Typechecking using ZML files

[<Pet...@ec...>]

Hi Tim,

On 02/12/11 14:59, Tim Miller wrote:
> Ok, I have solved this problem now (I think).

It has fixed my problem, thanks a lot!

Cheers,
Petra

Re: [CZT-Devel] Typechecking using ZML files

[Tim M. <tm...@un...>]

Ok, I have solved this problem now (I think). The typechecker was using 
object IDs in one place to determine if two types were the same, but 
because the parent was being parsed from XML, two equivalent types were 
being created, but with different object IDs.

I couldn't find a bug report on sourceforge -- did you submit one, Petra?

Regards,
Tim

On 14/10/11 02:31, Petra Dietrich wrote:
> On 13/10/11 16:54, Tim Miller wrote:
>> Petra, how are you running this? From the command-line tool?
>
> See attached files.
> If I put parent.zml and test.zed8 in the same directory (without
> parent.zed8 being available) and run
>
> java -jar czt.jar test.zed8
>
> I get:
> ERROR "test.zed8", line 3, column 18: Implicit parameters not determined
> 	Expression: dom
> ERROR "test.zed8", line 3, column 26: Implicit parameters not determined
> 	Expression: ∅
>
> However, parent.zml is generated from parent.zed8 using:
>
> java -jar czt.jar -o parent.xml parent.zed8
>
> and if parent.zed8 is available (that is, in the same directory so that
> czt can find it) it typechecks fine.
>
> Cheers,
> 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

Re: [CZT-Devel] schema composition type rule - query

[Mark U. <ma...@cs...>]

Leo,

Seems fine to me.  It is only the *matching* undashed-dashed pairs that are
unified.

In some kinds of framing schemas, it is useful to have other non-matching
primed (or unprimed) variables.

If you see a problem, you need to say what problem you see :-)

Mark


On 30 November 2011 03:38, Leo Freitas <leo...@ne...> wrote:

> Hi guys,
>
> I think there was discussion about this, but I don't know the details.
> From the Standard (13.2.6.22), I infer that
> the type for (LHS \semi RHS) is given by intricate filtering of bindings
> as follows:
>
> a) match = all the bindings of RHS that are NextStroke decorated in LHS
> (e.g., match set)
> b) B3       = LHS bindings  MINUS bindings of match decorated with
> NextStroke
> c) B4    = RHS bindings MINUS match
> d) result = B3 cup B4
>
> ex:
>
> S == [ x: \nat ]
> T == [ y: \nat ]
> LHS == [ \Delta S; in? : \nat ]
> RHS == [ \Delta S; out!: \nat ]
> Op == LHS \semi RHS
>
> what are the bindings of Op? I would expect them to be x, x', in?, out!
> but int I/O gets filtered out by the Std def?
> What if the composition is not homogenous like in
>
> LHS == [ \Delta S; \Delta T; in? : \nat ]
> RHS == [ \Delta S; out!: \nat ]
> Op == LHS \semi RHS
>
> or
>
> LHS == [ \Delta S;  in? : \nat ]
> RHS == [ \Delta S; \Delta T; out!: \nat ]
> Op == LHS \semi RHS
>
> bindings of Op given by the typechecker are x, x', y, y', in?, out!....
> That is despite the fact there might be more dashed
> variables in one side than the other. Any thoughts?
>
> Similarly, how to trust the definition for piping?
>
> Best,
> Leo
>
> ------------------------------------------------------------------------------
> 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. IT sense. And common sense.
> http://p.sf.net/sfu/splunk-novd2d
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>

[CZT-Devel] schema composition type rule - query

[Leo F. <leo...@ne...>]

Hi guys,

I think there was discussion about this, but I don't know the details. From the Standard (13.2.6.22), I infer that
the type for (LHS \semi RHS) is given by intricate filtering of bindings as follows:

a) match = all the bindings of RHS that are NextStroke decorated in LHS (e.g., match set)
b) B3       = LHS bindings  MINUS bindings of match decorated with NextStroke
c) B4 	 = RHS bindings MINUS match
d) result = B3 cup B4

ex:

S == [ x: \nat ]
T == [ y: \nat ]
LHS == [ \Delta S; in? : \nat ]
RHS == [ \Delta S; out!: \nat ]
Op == LHS \semi RHS

what are the bindings of Op? I would expect them to be x, x', in?, out! but int I/O gets filtered out by the Std def?
What if the composition is not homogenous like in 

LHS == [ \Delta S; \Delta T; in? : \nat ]
RHS == [ \Delta S; out!: \nat ]
Op == LHS \semi RHS

or 

LHS == [ \Delta S;  in? : \nat ]
RHS == [ \Delta S; \Delta T; out!: \nat ]
Op == LHS \semi RHS

bindings of Op given by the typechecker are x, x', y, y', in?, out!.... That is despite the fact there might be more dashed
variables in one side than the other. Any thoughts?

Similarly, how to trust the definition for piping?

Best,
Leo

[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
 		 	   		  

Re: [CZT-Devel] Typechecking using ZML files

[Petra D. <Pet...@ec...>]

On 13/10/11 16:54, Tim Miller wrote:
> Petra, how are you running this? From the command-line tool?

See attached files.
If I put parent.zml and test.zed8 in the same directory (without
parent.zed8 being available) and run

java -jar czt.jar test.zed8

I get:
ERROR "test.zed8", line 3, column 18: Implicit parameters not determined
	Expression: dom
ERROR "test.zed8", line 3, column 26: Implicit parameters not determined
	Expression: ∅

However, parent.zml is generated from parent.zed8 using:

java -jar czt.jar -o parent.xml parent.zed8

and if parent.zed8 is available (that is, in the same directory so that
czt can find it) it typechecks fine.

Cheers,
Petra

Re: [CZT-Devel] Typechecking using ZML files

[Tim M. <tm...@un...>]

It parses and typechecks fine for me, although I haven't checked whether 
the toolkit section is being re-typechecked,

Petra, how are you running this? From the command-line tool?

Cheers,
Tim

On 13/10/11 00:43, Petra Dietrich wrote:
> Hi,
>
> I am trying to typecheck a specification who's parent is given as a zml
> file that already contains type annotations.  Firstly, is my assumption
> that this should work without having to re-typecheck the parent right?
>
> Here is an example I am experimenting with:
>
> ─ section test parents toolkit └
> ─ ⊢? ∃x: ℙ(𝔸×𝔸) ⦁ dom x = ∅ └
>
> The toolkit parent is derived from standard_toolkit by just translating
> it to zml and renaming the Z section.  With standard_toolkit as parent,
> everything works well, but with toolkit (the zml version of
> standard_toolkit) I get the following error:
> ERROR "test.utf8", line 1, column 20: Implicit parameters not determined
> 	Expression: dom
> ERROR "test.utf8", line 1, column 28: Implicit parameters not determined
> 	Expression: ∅
>
> Any ideas what's going on?
>
> Thanks,
> 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

Re: [CZT-Devel] Typechecking using ZML files

[Petra D. <Pet...@ec...>]

Hi Leo,

Hmm, strange, it parses for me.  Maybe it is a problem with encoding or
something.  You can re-create the file on your system by just generating
the ZML file (with type annotations) for standard_toolkit and then
renaming it to toolkit.

Cheers,
Petra

On 13/10/11 05:23, Leo Freitas wrote:
> Hi Petra,
> 
> That's interesting. The XML itself wasn't even parsing (!) I was getting the error
> 
> "javax.xml.bind.UnmarshalException  - with linked exception: [org.xml.sax.SAXParseException: Content is not allowed in prolog.]"
> 
> within the command exception. That's interesting... I don't know where this is coming from (e.g., don't know about XML parsers);
> but I do know that ZML without type information does parse no problem (e.g., see examples in parser-zeves/*.zml)..... This error
> message sounds suspicious to me. Perhaps something wrong in the Jaxb XML generation involving types? Perhaps the fact
> the typechecker constructs different Type implementations from Corejava? I don't know.... :-(
> 
> Best,
> Leo

Re: [CZT-Devel] Typechecking using ZML files

[Leo F. <leo...@ne...>]

Hi Petra,

That's interesting. The XML itself wasn't even parsing (!) I was getting the error

"javax.xml.bind.UnmarshalException  - with linked exception: [org.xml.sax.SAXParseException: Content is not allowed in prolog.]"

within the command exception. That's interesting... I don't know where this is coming from (e.g., don't know about XML parsers);
but I do know that ZML without type information does parse no problem (e.g., see examples in parser-zeves/*.zml)..... This error
message sounds suspicious to me. Perhaps something wrong in the Jaxb XML generation involving types? Perhaps the fact
the typechecker constructs different Type implementations from Corejava? I don't know.... :-(

Best,
Leo

On 12 Oct 2011, at 14:43, Petra Dietrich wrote:

> Hi,
> 
> I am trying to typecheck a specification who's parent is given as a zml
> file that already contains type annotations.  Firstly, is my assumption
> that this should work without having to re-typecheck the parent right?
> 
> Here is an example I am experimenting with:
> 
> ─ section test parents toolkit └
> ─ ⊢? ∃x: ℙ(𝔸×𝔸) ⦁ dom x = ∅ └
> 
> The toolkit parent is derived from standard_toolkit by just translating
> it to zml and renaming the Z section.  With standard_toolkit as parent,
> everything works well, but with toolkit (the zml version of
> standard_toolkit) I get the following error:
> ERROR "test.utf8", line 1, column 20: Implicit parameters not determined
> 	Expression: dom
> ERROR "test.utf8", line 1, column 28: Implicit parameters not determined
> 	Expression: ∅
> 
> Any ideas what's going on?
> 
> Thanks,
> Petra
> <toolkit.zml><ATT00001..txt><ATT00002..txt>

[CZT-Devel] Animating Z Formal Specification

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

Hello, Petra, Leo.

I want to attach Formal Z specifications to the existing error localization and repair C++  project.
The error diagnosis requre reference model, that will generate referene outputs, what are used in diagnosis during comparison them with actual outputs.
This is basic idea of error diagnosis.

I want to make Formal Specifications written in Z to generate reference outputs. Using that the PhD will be much more full and i will have knowlege of formal specifications also.

The specifications i will create manually and will assume that they are generated somewhere somehow, i don't care how.
This requires just make the next steps:

1. Create specification.
2. Animate specification from c++ code using system c++ command.
3. Provide valid inputs (the format of inputs can be parameters that are sert at the moment of animation or data can be readed from file)
4. Recieve outputs.
5. Store outputs in valid format.
6. Continue diagnosis and repair using generated outputs.

The only one paragraph i have a problem - how to animate the specification.
I need to generate outputs from inputs using linux script, i will paste script to c++. I hope that CZT have this possibility, or i can use just parts of CZT that will animate the specification. Maybe it is possibly in specification write variables values to file?
I think its a good idea.

So for example if i have specification like
 ┌AddAB
 a?, b?, c!: ℕ
 |
 c! = a?+b?
 └

and input file with values
1 2
3 4
1 4
4 6
45 1

this will generate me
3
7
5
10
46

Thats all i need. The format of specification can be defined later.

ProZ - i need just to animate the specification prefably in ISO standart. So ZLive seems suitable. 

Urmas.

> From: leo...@ne...
> To: ur...@ho...
> CC: czt...@li...
> Date: Wed, 12 Oct 2011 16:29:20 +0100
> Subject: Re: [CZT-Devel] installing CZT
> 
> 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>
> 
 		 	   		  

Re: [CZT-Devel] installing CZT

[Leo F. <leo...@ne...>]

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>

[CZT-Devel] Typechecking using ZML files

[Petra D. <Pet...@ec...>]

Hi,

I am trying to typecheck a specification who's parent is given as a zml
file that already contains type annotations.  Firstly, is my assumption
that this should work without having to re-typecheck the parent right?

Here is an example I am experimenting with:

─ section test parents toolkit └
─ ⊢? ∃x: ℙ(𝔸×𝔸) ⦁ dom x = ∅ └

The toolkit parent is derived from standard_toolkit by just translating
it to zml and renaming the Z section.  With standard_toolkit as parent,
everything works well, but with toolkit (the zml version of
standard_toolkit) I get the following error:
ERROR "test.utf8", line 1, column 20: Implicit parameters not determined
	Expression: dom
ERROR "test.utf8", line 1, column 28: Implicit parameters not determined
	Expression: ∅

Any ideas what's going on?

Thanks,
Petra

Re: [CZT-Devel] installing CZT

[Petra D. <Pet...@ec...>]

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