czt-devel — For programmers using the CZT code

[CZT-Devel] Unexpected dependency on "TypeChecker .java"

[Leo F. <le...@cs...>]

Hi Tim and others,

I am including the Z TypeChecker into the Circus compiler and I noticed 
an unexpected
dependency on some object z classes, namely, 
net/sourceforge/czt/oz/ast/NameSignaturePair.

The problem happen during the instantiation of the class
net.sourceforge.czt.typecheck.z.TypeChecker at the line 102

"predChecker_ = new PredChecker(this);"

I also noticed that the factory implementation in 
net.sourceforge.czt.typecheck.util.impl,
also enforce that Z specifications will need to include the ObjectZ Jar 
file!

As I will not consider ObjectZ for Circus, is there any way around the 
ObjectZ dependency?

Thanks.
Leo

[CZT-Devel] Updated CZT proof rules proposal (committed)

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

Dear CZT'ers,

I've commited a new version of the CZT proof rules proposal into the CVS 
repository (doc/papers/rules).  Hopefully you can just check it out and 
run it through LaTeX.

It has a large amount of changes, including:
1.  A CUP-like grammar for Tim to think about / work on.
2.  A lot more details about the syntax of rules, including LaTeX and 
Unicode markups.
3.  More powerful provisos (side-conditions) that allow us to calculate 
schema compositions in a single bound (cf. Superman).  Here is this 
Superman rule (though it probably will not be understandable until you 
read the document!):

>
> \begin{zedrule}{SemiInOneStep}
>   \proviso hide == removedecor(primevars(\alpha[D1]))
>                    \cap undecorvars(\alpha[D2]) \\
>   \proviso hidden == fresh~hide \\
>   \proviso P1b == P1 \substitute \lblot hide' == hidden \rblot \\
>   \proviso P2b == P2 \substitute \lblot hide' == hidden \rblot \\
>   \proviso D1r == D1 \hide (hide') \\
>   \proviso D2r == D2 \hide (hide) \\
>   \proviso D == [D1r;D2r] \\
>   \proviso D1h == (D1 \filter(hide'))\substitute\lblot hide' == hidden 
> \rblot\\
>   \proviso D2h == (D2 \filter(hide))\substitute\lblot hide == hidden 
> \rblot\\
>   \proviso D3 == [D1h;D2h]
>   \derives
>   [D1|P1] \semi [D2|P2] = [ D | (\exists [D3] @ P1 \land P2)]
> \end{zedrule}
>

I have not addressed Petra's questions about the Deduction interface yet.

Also, the paper discusses two alternative ways of searching for 
defns/predicates in a context/specification.  I've assumed that we will 
use the first one (with an explicit 'lookup' proviso), but it would be 
good to have some discussion about the pros and cons of the two approaches.

Happy reading?  :-)
Mark.

[CZT-Devel] Re: putting PrintUtils to work in toString()

[Petra M. <pe...@cs...>]

Hi again,

Leo Freitas wrote:
>            PrintUtils.printLatex(e, swr, sm);

This method will only work properly for Sect and Spec elements, i.e. 
terms that contain a section header (it should be mentioned in the 
Javadoc documentation).

To print an arbitrary expression, a kind of context must be given. 
That's because the printer needs to know things like the precedence and 
associativity of the operators used, etc.

Try,
PrintUtils.printLatex(e, swr, sm, "standard_toolkit")
instead. This should work when your Expr do only use operators defined 
in the standard_toolkit.

> Moreover, I tried to compile/build the parser package outside the main 
> Czt build.xml but with the one of the parser package.
> it keep complaining that the net.sourceforge.czt.java_cup.runtime is not 
> available or couldn't be found. Any clue on reasons for this?

The parser cannot build alone. It does depend on other subprojects in 
CZT like, for example corjava and java_cup. If you don't want to use the 
top level build script, you can build the subprojects independently, but 
you need to do it in the right order. java_cup is in 
<CZT_HOME>/devtools/java_cup.
Change into this directory and call ant. This should build the jar file
<CZT_HOME>/lib/java_cup.jar
which is needed to build the parser.
It's still better to use the top level build script ... it will make 
sure that everything is build in the right order. After that you can 
change into the parser directory and rebuilding the parser should work well.

Hope that helps,
Petra

[CZT-Devel] putting PrintUtils to work in toString()

[Leo F. <le...@cs...>]

Hi all,

I've got an implementation of sets that contain Z:Expr as elements.
Following the code from PrintUtils in the parser package and similar 
sources,
I created the following code:

 public String toString() {       
        SectionManager sm = new SectionManager();
        StringWriter swr = new StringWriter();        
        swr.write("ZSet == \n\t{");
        for (Iterator it = members(); it.hasNext(); ) {
            Expr e = (Expr)it.next();
            PrintUtils.printLatex(e, swr, sm);            
        }
        swr.write("}");    
        try {
            swr.close();
        }
        catch (IOException e) {
            System.err.println("I/O Error while trying to print ZSet; it 
should never happen.");
        }
        return swr.toString();
}

Is this right?
Assuming that the set contains one element as a pair, say (x, y) from a 
ProdExpr with a code such as

        Factory f = new Factory();
        HashSetZSet s = new HashSetZSet();       
        Expr prod = 
f.createProdExpr(f.list(f.createRefExpr(f.createRefName("x")), 
f.createRefExpr(f.createRefName("y"))));
        s.add(prod);
        System.out.println(s.toString());

I get the following error at the printLatex call:

Error (30,x): Syntax error
Error (30,x): Couldn't repair and continue parse
Exception in thread "main" net.sourceforge.czt.util.CztException: 
java.lang.UnsupportedOperationException: Parse error.
    at net.sourceforge.czt.print.z.PrintUtils.printLatex(PrintUtils.java:72)
    at 
circus.modelchecker.compiler.base.HashSetZSet.toString(HashSetZSet.java:259)
    at 
circus.modelchecker.compiler.base.HashSetZSet.main(HashSetZSet.java:275)
Caused by: java.lang.UnsupportedOperationException: Parse error.
    at 
net.sourceforge.czt.print.z.Unicode2Latex.report_fatal_error(Unicode2Latex.java:479)
    at 
java_cup.runtime.lr_parser.unrecovered_syntax_error(lr_parser.java:409)
    at java_cup.runtime.lr_parser.parse(lr_parser.java:601)
    at net.sourceforge.czt.print.z.PrintUtils.printLatex(PrintUtils.java:69)
    ... 2 more
Java Result: 1

Is this a bug in the way I am creating expressions? I want to pretty 
print the expression elements of the set. what is the missing bit?
Moreover, I tried to compile/build the parser package outside the main 
Czt build.xml but with the one of the parser package.
it keep complaining that the net.sourceforge.czt.java_cup.runtime is not 
available or couldn't be found. Any clue on reasons for this?

thanks
Leo

[CZT-Devel] Re: Parser: Integrating Circus.cup into Parser.xml

[Petra M. <pe...@cs...>]

Hi Leo,

Leo Freitas wrote:
> I noticed that there are 14 ant tasks associated to parser generation.
> How many of those I need to be worried about? In other words, apart from 
> the Parser.xml
> file, what other files do I need to change? Perhaps this is in direct 
> connection with the next question.

You need all of them, but you won't need to edit all corresponding xml 
files. I added all required circus tasks to the build.xml file and 
commited it to CVS, so you don't have to worry about that.

> 1) LaTeX Markup
> 
> In Circus, there are environments for declaring new circus paragraphs as 
> \begin{circus}...\end{circus},

The CZT parser for LaTeX markup consists of a LaTex to Unicode converter 
  followed by a Unicode scanner and parser. That's because the Z grammar 
given in the ISO Standard is defined for Unicode only.
That means, you need to think about how a circus specification is 
supposed to look like in Unicode.

Since Unicode characters are difficult to type (using an editor that 
doesn't support Unicode), all Unicode charcters used in Z (or OZ, TCOZ) 
got a name. These are defined in <CZT_HOME>/devtools/zchar.xml (or 
<CZT_HOME>/devtools/ozchar.xml, CZT_HOME>/devtools/tcozchar.xml).

These XML files are used to generate the corresponding classes
net.sourceforge.czt.z.util.{ZChar,ZString}
net.sourceforge.czt.oz.util.{OzChar,OzString}
net.sourceforge.czt.tcoz.util.{TcozChar,TcozString}

So I guess we need to write a circuschar.xml file where Circus specific 
Unicode characters are listed. Tim might be able to help with this ... 
he has done that for Object Z.

To define the \begin{circus} ... \end{circus} paragraphs, we need to 
modify the LaTeX to Unicode converter. It's in
parser/templates/Latex2Unicode.xml.

Next, the Unicode scanner needs to know about Circus. The Unicode 
scanner consists of the context-free scanner followed by other kinds of 
scanners. The context-free scanner is in
parser/templates/ContextFreeScanner.xml.



Just to get you started, I added all the stuff to the scanner and parser 
so that
----------------------------------------
\begin{zed}
   \vdash?~true
\end{zed}

\begin{circus}
   x : \nat
\end{circus}
----------------------------------------

can now be parsed (with the Circus parser) and the resulting XML looks like

<Spec Version="1.3" xmlns="http://czt.sourceforge.net/zml">
     <ZSect>
         <Name>Specification</Name>
         <Parent>
             <Word>standard_toolkit</Word>
         </Parent>
         <LatexMarkupPara/>
         <ConjPara>
             <TruePred/>
         </ConjPara>
         <ns1:ChannelPara xmlns:ns1="http://czt.sourceforge.net/circus">
             <VarDecl>
                 <DeclName>
                     <Word>x</Word>
                 </DeclName>
                 <RefExpr Mixfix="false">
                     <RefName>
                         <Word><E2><84><95></Word>
                     </RefName>
                 </RefExpr>
             </VarDecl>
         </ns1:ChannelPara>
     </ZSect>
</Spec>

You can try that by calling "ant circus2zml" in the parser directory.

Hope that gives you a bit of a start,
Petra

[CZT-Devel] Re: Bean shell bug?

[Petra M. <pe...@cs...>]

Hi Leo,

Leo wrote:
> While playing around with bean shell I noticed that the "showTree" 
> method opens a frame without a scroll bar on the right-hand side.
> That makes browsing of bigger specifications nearly impossible because 
> they tend to go off the screen.
> Is this a bean shell problem or could it be ammended in the CZT itself?

This is not really a bug, it was just not yet implemented.
The "showTree" command is implemented by a very simple beanshell script. 
It's in <CZT_HOME>/bin/bsh/showTree.bsh
in the CVS repository. I just commited a version that also uses scrollbars.

Feel free to improve the scripts further, they are still very simple and 
just outline what could be done.

Cheers,
Petra

[CZT-Devel] Parser: Integrating Circus.cup into Parser.xml

[Leo F. <le...@cs...>]

Hi all,

I am having a go at including the circus parser within the CZT 
framework, and I've got some questions.
Sorry for it to be a bit (7 questions) long. I am not really used to 
CUP. I tried to make them as general as possible.
I will attach the original Circus.cup file as well as the altered 
Parser.xml file including the <add:circus> tags.

0) Ant scripts for building the files

I noticed that there are 14 ant tasks associated to parser generation.
How many of those I need to be worried about? In other words, apart from 
the Parser.xml
file, what other files do I need to change? Perhaps this is in direct 
connection with the next question.

1) LaTeX Markup

In Circus, there are environments for declaring new circus paragraphs as 
\begin{circus}...\end{circus},
as well as new LaTeX macros such as \circchannel, \circprocess, 
\circend, etc...
What is necessary to include those appropriately?
In the original Circus.cup file I realised that there are terminal 
tokens in the CUP file with a
corresponding JFlex scanner with the rules. Moreover, I also realised 
that the scanning on CZT is
rather complex due to issues of the Z std mentioned in some CZT articles.
In this sense, what are the appropriate place (XML template) to adjust?
I guessed about the KeywordScanner, and started a trial-and-error 
approach, but then I saw
that it is not as simple as the Circus.flex version... Any help on this?

2) Default/Initial environments for operators (i.e. DefinitionTable?)

I noticed tat CZT has initial (preloaded) operations perhaps divided by 
Z:Sect, is that right?
Well, in Circus there are a couple of predefined expressions such as the 
type of synchronisation channels.
It is just something like a given set such as "[Synch]", where channel 
declarations with a corresponding type
as in

channel c

will in fact be covered in the grammar as:

channe c: Synch

I tried to create this expression on the fly with the code

    private Expr getSynchExpr() {
      return 
factory_.createSetExpr(factory_.list(factory_.createRefExpr(factory_.createRefName("Synch"))));
    }

inside the "action code" section of Parser.xml. the expressions come 
from the inspection in bean shell of the AST generated for
[Synch]
\begin{axdef}
    synchType: \{Synch\}; synchValue: Synch
\where
    synchValue \in synchType
\end{axdef}

3)  Comma-separated Declarations.

Circus contains numerous places where comma separated declarations are 
expected, for example channel declarations.
I noticed that, differently from the Circus.cup file that treat lists 
directly (see "cDecl" production in circus.cup), the CZT deals with list
of declarations with List's on the fly (eg. "declPar" production). How 
does the CZT parser interpret these lists?

Furthermore, I saw that the production "basicDeclaration" in Parser.xml 
is somewhat similar to waht I need.
However, because I want to differentiate the two cases with and without 
an expression for the channel type I simply copied
one of the values of the "basicDeclaration" production and performed the 
ammendments (see "simCDecl" in circus.cup and "simCDecl" in Parser.xml).
Is this the appropriate way?

4) What is the import "net.sourceforge.czt.tcoz.util.TcozString" for? I 
couldn't find it in the CZT distribution. Do I need something similar?

5) Channel declarations

Why is it that in TCOZ channel declarations are given inside the "term 
::=" nonterminal production?
 From the BNF of TCOZ, as far as I could understand, channels can only 
be declared within a StateSchema production.
Circus also have channel declarations but as a paragraphs that can 
declared anywhere outside a process (i.e. any place where Z:Para is 
accepted).
So, I think I should use the additional production:
        |
        INICIRC chanPara: cp ENDCIRC
        {:
            RESULT = cp;
        :}
to unboxedParagraphItem of Parser.xml.

6)
 From Circus.cup, productions "chanDef" and "cDecl" are given as 
ChannelPara.
However, since I tried to use the CZT way of including list separated 
values, what type should these have?
I tried with "List"  and "ChannelPara", but both failed given the output 
below, any idea why?

Opening files...
Parsing specification from standard input...
Checking specification...
Building parse tables...
  Computing non-terminal nullability...
  Computing first sets...
  Building state machine...
  Filling in tables...
  Checking for non-reduced productions...
Writing parser...
Closing files...
------- CUP v0.10k Parser Generation Summary -------
  0 errors and 0 warnings
  99 terminals, 109 non-terminals, and 273 productions declared,
  producing 509 unique parse states.
  0 terminals declared but not used.
  0 non-terminals declared but not used.
  0 productions never reduced.
  0 conflicts detected (0 expected).
  Code written to "Parser.java", and "Sym.java".
---------------------------------------------------- (v0.10k)
java.lang.Exception: Parser could not be written to 
D:\research\tools\java\sourceforge\czt\cvs.czt.adv\parser\build\src\net\sourceforge\czt\parser\circus\Parser.java
    at ant.JavaCupTask.execute(JavaCupTask.java:140)
    at org.apache.tools.ant.UnknownElement.execute(UnknownElement.java:275)
    at org.apache.tools.ant.Task.perform(Task.java:364)
    at org.apache.tools.ant.Target.execute(Target.java:341)
    at org.apache.tools.ant.Target.performTasks(Target.java:369)
    at org.apache.tools.ant.Project.executeTarget(Project.java:1214)
    at org.apache.tools.ant.Project.executeTargets(Project.java:1062)
    at 
org.apache.tools.ant.module.bridge.impl.BridgeImpl.run(BridgeImpl.java:217)
    at 
org.apache.tools.ant.module.run.TargetExecutor.run(TargetExecutor.java:236)
    at 
org.netbeans.core.execution.RunClassThread.run(RunClassThread.java:125)
D:\research\tools\java\sourceforge\czt\cvs.czt.adv\parser\build.xml:829: 
Java cup failed!

Best regards,
Leo

[CZT-Devel] Bean shell bug?

[Leo F. <le...@cs...>]

Hi there,
While playing around with bean shell I noticed that the "showTree" 
method opens a frame without a scroll bar on the right-hand side.
That makes browsing of bigger specifications nearly impossible because 
they tend to go off the screen.
Is this a bean shell problem or could it be ammended in the CZT itself?

thanks,
leo

[CZT-Devel] Re: CZT Parser(s) - Circus extension

[Petra M. <pe...@cs...>]

Hi,

Leo wrote:
> I guess that I need to include another branch in the ant task Petra
> produced to cover circus, is that right? I mean, once I have included
> a new production into the XML files, what are the steps to follow to
> produce the parser class?  ... Just include something like
> 
> <target name="generate-circus-parser" depends="circus-parser, 
> circus-lparser, circus-uparser, circus-parserutils"/>
> 
> (plus the related targets) and then run the ant scripts?

Yes, that's it. :-)

For example, the Circus java_cup source is build by a target like this:

<target name="circus-parser-cup" depends="init">
   <xslt
     in="templates/Parser.xml"
     out="${build.src.circus.dir}/Parser.cup"
     style="${czt.home}/devtools/template2text.xsl">
     <param name="class" expression="Parser"/>
     <param name="package"
            expression="net.sourceforge.czt.parser.circus"/>
     <param name="add" expression="{circus}"/>
   </xslt>
</target>

As you can see, the .cup file is generated by applying the XSL script
devtools/template2text.xsl to the parser/templates/Parser.xml file.
Params "class" and "package" are used to set the class and package name 
of the parser to be generated. I suggest to use a Circus package for 
your parser as shown above.

Param "add" selects the parser version to be generated.  Your parser 
needs, in addition to the Standard Z parser code, all code included in 
<add:circus> tags. It is also possible to have a list of tags that 
should be added as, for example, in "{oz}{tcoz}".

Setting up the build file shouldn't be too difficult. I can do that for 
you if you want.

Cheers,
Petra

Re: [CZT-Devel] CZT Parser(s) - Circus extension

[Leo F. <le...@cs...>]

Hi Tim,

>> What I would like to do is to integrate the code of this parser 
>> within the parsing structure available in the CZT.
>> As far as I could understand, there are some XML template files and 
>> the ant build script that generates the parser codes.
>> Is there a kind of GnAST for generating parsers as well, or is it a 
>> sort of XML transformation that is necessary?
>
> The parser is written using an XML file. There is a base Z-part to the 
> parser file, and rules for Z extensions are put between tags. For 
> example, in the Object-Z parser, Object-Z paras/exprs etc are put 
> between <add:oz> </add:oz> tags. Petra has set up some neat trick in 
> the ant script that generates Object-Z and TCOZ CUP grammars from this 
> file.  The parser XML file is in parser/templates/Parser.xml

thanks for that. I will study this closely soon and will try to include 
the Circus productions there.
I guess that I need to include another branch in the ant task Petra 
produced to cover circus, is that right?
I mean, once I have included a new production into the XML files, what 
are the steps to follow to produce the parser class?
I know I need to run java cup over the cup file and so on, but since we 
are using XML and ant (something I haven't come across before),
what to do in the ant script? Just include something like

  <target name="generate-circus-parser"
    depends="circus-parser, circus-lparser, circus-uparser, 
circus-parserutils"/>

(plus the related targets) and then run the ant scripts?

>>  From the ant script it seems more like the. If that is so, what are 
>> the files I need to modify to take the Circus CUP into account?
>
> Most of the files in the parser/templates directory I think. You will 
> need to edit the scanner (which is implement over several XML files), 
> as well as the parser grammar.

Ok.

>> I know a little about CUP and grammars, but never used them. I am 
>> aware that dealing with CUP is not a task as easy as creating the 
>> Circus.xsd file.
>> It includes all that shift/reduction rules and conflicts to be 
>> solved. As the Z standard is already implemented in the CZT and some 
>> examples of extension are available,
>> I am assuming that including Circus CUP productions is somehow  
>> straightforward. Am I being overoptimisitic?
>> Is there anyone interested in helping doing this integration?
>
> A lot of the precedence problems are Z related, and from what I know 
> of CSP, a CSP extension to Z shouldn't be too difficult (as far 
> parsing goes) if it's built on a Z parser.

That is my intuition too.

> I'm just looking at your Circus XML schema, and I think you can do a 
> few things in there to make the transition easier. For starters, I 
> don't think you really need CircusSect or CircusPara. The best 
> solution would be to have channel, channel set, and process paragraphs 
> extend Z:Para. Even though you comment that Circus paragraphs are not 
> allowed within process definitions, the parser grammar can restrict 
> this. This simplifies the AST classes, and any other tools that use 
> them (e.g. less classes to write visitor methods for, and also you can 
> write tools such as a circus typechecker by extending the visitor 
> classes in the Z typechecker).

That is right. I was discussing this with Petra in another e-mail. I 
guess that is right.
When I wrote the schema, I followed the CUP grammar productions as well 
as the BNF of Circus I had at hand.
At first I thought they insisted on the differentiation of CircusPara, 
but with a closer look at the CUP file and your suggestions,
I could see that this differention is not the case. The confusion 
perhaps came from the fact that although Circus is a superset of Z,
the CUP grammar assumes Circus as a superclass of Z and not the other 
way round like the CZT does!

> If you remove these classes, then the parser becomes much easier to 
> extend too. You add the three new paragraphs to the "paragraph" rule 
> in the grammar, and then add a new rule called "processExpr" or 
> something (I guess processes aren't really expressions but something 
> along those lines). The "processExpr" rule will be straightforward 
> because this will not conflict with any of the Z rules, and also, it 
> is VERY similar to several of the Z, Object-Z, and TCOZ rules already 
> in the parser :)

I am pleased to hear that! Parsing is not really my first priority at 
the moment, but I am really interested in integrating Circus with the CZT.
And since I just recieve the working Circus parser, I thought to have a 
go at it using the CZT facilities.

> So firstly, I suggest you check the parser project out from the CVS 
> server and have a look how it is designed. Then try to add some of the 
> Circus extensions, but add only a few at a time, and then make sure 
> they work before continuing.
> I'm happy to answer any questions you have. I wrote most of the Z and 
> Object-Z grammar that are there, and Petra wrote most of the 
> supporting code and the scanner, so between us we should be able to 
> help with any problems.

Great! I will try those out soon and I let you know.

> Regards,
> Tim

Best regards,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Computer Science @ York University
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------

Re: [CZT-Devel] CZT Parser(s) - Circus extension

[Tim M. <ti...@cs...>]

Hi Leo,

> What I would like to do is to integrate the code of this parser within 
> the parsing structure available in the CZT.
> As far as I could understand, there are some XML template files and the 
> ant build script that generates the parser codes.
> Is there a kind of GnAST for generating parsers as well, or is it a sort 
> of XML transformation that is necessary?
The parser is written using an XML file. There is a base Z-part to the 
parser file, and rules for Z extensions are put between tags. For 
example, in the Object-Z parser, Object-Z paras/exprs etc are put 
between <add:oz> </add:oz> tags. Petra has set up some neat trick in the 
ant script that generates Object-Z and TCOZ CUP grammars from this file. 
  The parser XML file is in parser/templates/Parser.xml

>  From the ant script it seems more like the. If that is so, what are the 
> files I need to modify to take the Circus CUP into account?
> 
Most of the files in the parser/templates directory I think. You will 
need to edit the scanner (which is implement over several XML files), as 
well as the parser grammar.

> I know a little about CUP and grammars, but never used them.
> I am aware that dealing with CUP is not a task as easy as creating the 
> Circus.xsd file.
> It includes all that shift/reduction rules and conflicts to be solved.
> As the Z standard is already implemented in the CZT and some examples of 
> extension are available,
> I am assuming that including Circus CUP productions is somehow  
> straightforward. Am I being overoptimisitic?
> Is there anyone interested in helping doing this integration?
> 
A lot of the precedence problems are Z related, and from what I know of 
CSP, a CSP extension to Z shouldn't be too difficult (as far parsing 
goes) if it's built on a Z parser.

I'm just looking at your Circus XML schema, and I think you can do a few 
things in there to make the transition easier. For starters, I don't 
think you really need CircusSect or CircusPara. The best solution would 
be to have channel, channel set, and process paragraphs extend Z:Para. 
Even though you comment that Circus paragraphs are not allowed within 
process definitions, the parser grammar can restrict this. This 
simplifies the AST classes, and any other tools that use them (e.g. less 
classes to write visitor methods for, and also you can write tools such 
as a circus typechecker by extending the visitor classes in the Z 
typechecker).

If you remove these classes, then the parser becomes much easier to 
extend too. You add the three new paragraphs to the "paragraph" rule in 
the grammar, and then add a new rule called "processExpr" or something 
(I guess processes aren't really expressions but something along those 
lines). The "processExpr" rule will be straightforward because this will 
not conflict with any of the Z rules, and also, it is VERY similar to 
several of the Z, Object-Z, and TCOZ rules already in the parser :)

So firstly, I suggest you check the parser project out from the CVS 
server and have a look how it is designed. Then try to add some of the 
Circus extensions, but add only a few at a time, and then make sure they 
work before continuing.

I'm happy to answer any questions you have. I wrote most of the Z and 
Object-Z grammar that are there, and Petra wrote most of the supporting 
code and the scanner, so between us we should be able to help with any 
problems.

Regards,
Tim

[CZT-Devel] Re: zlive sets

[Petra M. <pe...@cs...>]

Hi Leo,

Leo wrote:
> In zlive set implementations for EvalSet interface, I noticed there are 
> corresponding visitor classes
> (eg. FlatDiscreteSetVisitor). I couldn't find any examples (or Javadoc) 
> of using such visitors.

You can find a general introduction into the visitor design pattern used 
in CZT in our ZB 2005 paper:
CZT---A Framework for Z Tools
I will send you a copy of this.

> For waht purpose they were introduced?

FlatDiscreteSet extends FlatPred which extends Pred and therefore Term. 
That is, a FlatDiscreteSet needs to implement the method
   Object accept(Visitor visitor);
defined in the Term interface. To be properly visitable one needs the
FlatDiscreteSetVisitor interface.

I do not know what Mark is planning to do with FlatDiscreteSets, but 
almost every tool that traverses an AST is implemented as a visitor.

Cheers,
Petra

[CZT-Devel] CZT Parser(s) - Circus extension

[Leo F. <le...@cs...>]

Hi all,

I am now with the parser for Circus written using CUP and JLex similar 
to the one available in the CZT.
It recognises Circus programs where the Z part is in comformance with 
the Z standard.
The point is that although the generated AST is in comformance with Z 
standard, it is not in comformance
with CZT AST classes, nor does it has visiting facilities.
The Circus.xsd file is very much based in the CUP file with some 
adjustments to properly integrate with the CZT.

What I would like to do is to integrate the code of this parser within 
the parsing structure available in the CZT.
As far as I could understand, there are some XML template files and the 
ant build script that generates the parser codes.
Is there a kind of GnAST for generating parsers as well, or is it a sort 
of XML transformation that is necessary?
 From the ant script it seems more like the. If that is so, what are the 
files I need to modify to take the Circus CUP into account?

I know a little about CUP and grammars, but never used them.
I am aware that dealing with CUP is not a task as easy as creating the 
Circus.xsd file.
It includes all that shift/reduction rules and conflicts to be solved.
As the Z standard is already implemented in the CZT and some examples of 
extension are available,
I am assuming that including Circus CUP productions is somehow  
straightforward. Am I being overoptimisitic? 

Is there anyone interested in helping doing this integration?

All the best,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Computer Science @ York University
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------

[CZT-Devel] zlive sets

[Leo F. <le...@cs...>]

Hi all,

In zlive set implementations for EvalSet interface, I noticed there are 
corresponding visitor classes
(eg. FlatDiscreteSetVisitor). I couldn't find any examples (or Javadoc) 
of using such visitors.
For waht purpose they were introduced? By allowing visiting, I assume it 
as general form to allow operations over sets (Operation Adder Pattern).
That is, one can use the visitor to add elements, remove elements, order 
elements, transform predicates, print the set, and so on. Is that right ?

Thanks,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Computer Science @ York University
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------

[CZT-Devel] GnAST and complete Circus.xsd

[Leo F. <le...@cs...>]

Hi Petra and others,

I made the necessary ammendments and inclusions into the Circus.xsd file 
as we discussed.
Furthermore, I have also included the complete (current) BNF of Circus 
with the whole
action and process language.
Besides the usual CSP operators for Actions, it includes CSP operators 
for Processes,
new Circus operators for Processes, the complete guarded commands 
(assignment, if,
specification statement, etc), and others.

I could also put GnAST to run and I have generated the Circus AST and 
Visitors nicely!
GnAST only issued a warning saying that "Expt0N" could not be found in Z 
context/prefix.
I couldn't figure out why tough.
I should include some more documentation in the schema file soon.

Thanks for all the help given!

Best regards,
Leo
-- 

-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Computer Science @ York University
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------

Re: [CZT-Devel] Evaluating Z in Java

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

Hi Leo,

You wrote:

> I am interested in the development of a z-evaluation tool similar to 
> Jaza (by Mark) in Java.
> Moreover, is there any interest in working on the development of  a 
> Z-toolkit in Java?
> Is there any work in these fronts? If so, any 
> plans/architecture/models for it already?
> If not, apart from Jaza, JML and Jakarta-Common-Collections, do you 
> know of
> any other interesting sources on this? I would be very interested in 
> participating.

Great!  We would love to have you work on this too.
As Petra mentioned, we have made a start on writing something similar to 
Jaza
(but better of course -- I hope the new architecture will be simpler and 
more flexible)
in Java.  You can see the code that we've written so far in the zlive 
directory.

(By the way, my favourite CVS interface under Windows is TortoiseCVS,
from www.*tortoisecvs*.org.  If you install this, here are the steps to 
get a full
checkout of the CZT sources: 
    1. create a directory (eg. CZT).
    2.  right-click on that directory and choose "CVS Checkout" from the 
menu
    3.  fill in the parameters, as described on the sourceforge web page 
that Tim mentioned:
            http://sourceforge.net/cvs/?group_id=86250
             If you tell us your sourceforge login (bikerider?), we will 
add you as a developer,
             then you can use the Developer CVS access and make 
changes.  Until then,
             start by using the anonymous pserver access, as follows:
          Eg.  Protocol:   pserver
                 Server:  cvs.sourceforge.net
                 Port:   (default will work)
                 Repository folder:  /cvsroot/czt
                 User name:  anonymous
                 Module:     .                     (to get everything!)
  4.   Click OK and watch thousands of files get downloaded.
         You'll need about 100Mb of disk to build all of CZT.
)

(The next step is to read the README, then install various
utilities and libraries, and edit czt.properties to say where you
have put them).

>
> This Z evaluator will be used as part of the development of a 
> model-checker for Circus, a language that
> combines CSP and Z in the unifying theories of programming. After 
> working in the theoretic background,
> we are now at the implementation stage. Eventually, we expect this to 
> become a sort of Z-Evaluator/Prover.

Excellent.  I'm glad to see that you've been working with
Petra on the XML schema for Circus.  This is the first step
to getting Circus built on top of CZT.

Yes, ZLive is our rewrite of Jaza into CZT.
It is currently capable of animating/evaluating arithmetic expressions and
simple set comprehensions.   The basic architecture is that the Flatten 
class
(zlive/src/net/sourceforge/czt/animation/eval/Flatten.java) recurses through
the Z AST and creates a list of 'FlatPred' objects, one for each operator.
These 'FlatPred' objects are capable of evaluating the operator in different
'modes' (different combinations of inputs and output).  For example, the
+ operator (Res = A+B) could be evaluated with A,B as inputs and
Res as output, or Res and A as inputs (so the output B would be evaluated
as Res-A, or Res and B as inputs, or all three as inputs.  This is like
a constraint-logic programming approach.

I have some slides describing the design of ZLive, so will send these to
you.  But we will probably need some more discussion before you've
got enough to understand what to do next.  I'd like to work with you
on this, and can suggest some papers to read to give some background
on the mode analysis etc.

Another project going on in parallel is to see if we can translate
Z into SAL (see fm.csl.sri.com).  Graeme Smith is working on this and
so am I.  This would also give some limited animation facilities, but is 
more
aimed at model-checking.  So I think that the two approaches will be
reasonably complementary.

I look forward to keeping in touch with you.
Let us know of any practical problems you have...
Mark.

[CZT-Devel] Re: Evaluating Z in Java

[Petra M. <pe...@cs...>]

Hi Leo,

Leo Freitas wrote:
> I am interested in the development of a z-evaluation tool similar to 
> Jaza (by Mark) in Java.
> Moreover, is there any interest in working on the development of  a 
> Z-toolkit in Java?

Mark is working on a new animator written in Java, which is based on the 
CZT corejava classes. I hope he will answer your questions in more detail.
His new animator is called zlive, and the source code can be found in 
the CZT CVS repository (subdirectory zlive).

Cheers,
Petra

[CZT-Devel] Re: GnAST and other Z tools of CZT

[Petra M. <pe...@cs...>]

Hi Leo,

Leo Freitas wrote:
> I am developing a XML-Schema to represent Circus, a language that 
> combines CSP
> and Z, and I would like to try to use GnAST on this XML-schema.

Nice!
I am very interested in having a look at your Schema.
Are you extending our ZML XML Schema?
Perhaps we can set up a subproject of CZT for Circus
if you are willing to put your code under the GPL license.

> Are you aware of when GnAST and other tools such as the
> Z-Parser/Typechecker will be available in the CZT distributtion?

GnAST is not designed to generate classes from arbitrary XML Schemas.
There are many restrictions on the XML Schema, which are not documented, 
and the error messages provided by GnAST are probably not very helpful 
either. That's why we are not planning to release GnAST in the near future.

However, the source code of GnAST is available in CVS (you should really 
try to get used to CVS; it is worth the effort).
The easiest thing would probably be to send your Schema to me and I will 
try to generate classes from it.

Note that there are two sets of classes and interfaces. There are the 
classes generated by GnAST located in packages 
net.sourceforge.czt.<subproject>.ast
net.sourceforge.czt.<subproject>.impl and
net.sourceforge.czt.<subproject>.visitor.
And there are JAXB (https://jaxb.dev.java.net/) generated classes 
located in package
net.sourceforge.czt.<subproject>.jaxb.gen.
Of course, you can try JAXB on your XML Schema without using GnAST.

The JAXB classes are used to read and write XML, and GnAST also 
generates visitors that can transform a tree of JAXB classes into a tree 
of GnAST generated classes and the other way round.

I hope that GnAST becomes obsolete in the near future as tools like JAXB 
get more and more customizable, making it possible to generate exactly 
the classes we want.

Hope that helps,
Petra

Re: [CZT-Devel] GnAST and other Z tools of CZT

[Tim M. <T.M...@cs...>]

Hi Leo,

Leo Freitas wrote:

> I am developing a XML-Schema to represent Circus, a language that 
> combines CSP
> and Z, and I would like to try to use GnAST on this XML-schema.
> 
Great!

> Are you aware of when GnAST and other tools such as the
> Z-Parser/Typechecker will be available in the CZT distributtion?

As far as I know, Petra has no plans to release Gnast in the CZT 
distribution. It was only written to generate the Z, Object-Z, 
etc, core classes for CZT really. The parser/typechecker are 
available in binary format for download 
(http://www.cs.waikato.ac.nz/~petra), but I'm not sure if Petra 
has any plans for a source release in the near future.

> I tried to set up the WinCVS but I am finding some difficulties here,
> as I am still in the learning process of using CVS.......
> 
I've never used WinCVS, but I can direct you here:
https://sourceforge.net/cvs/?group_id=86250

and here:
https://sourceforge.net/docman/display_doc.php?docid=14033&group_id=1

If these are no help, email me directly and I will send you a 
tarball with the gnast code so you can play around with it while 
you figure out your CVS problems.

Regards,
Tim

[CZT-Devel] GnAST and other Z tools of CZT

[Leo F. <le...@cs...>]

Dear CZT users,

I am developing a XML-Schema to represent Circus, a language that 
combines CSP
and Z, and I would like to try to use GnAST on this XML-schema.

Are you aware of when GnAST and other tools such as the
Z-Parser/Typechecker will be available in the CZT distributtion?
I tried to set up the WinCVS but I am finding some difficulties here,
as I am still in the learning process of using CVS.......

Best regards,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Computer Science @ York University
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------

[CZT-Devel] Evaluating Z in Java

[Leo F. <le...@cs...>]

Dear Petra, Tim and others

I am interested in the development of a z-evaluation tool similar to 
Jaza (by Mark) in Java.
Moreover, is there any interest in working on the development of  a 
Z-toolkit in Java?
Is there any work in these fronts? If so, any plans/architecture/models 
for it already?
If not, apart from Jaza, JML and Jakarta-Common-Collections, do you know of
any other interesting sources on this? I would be very interested in 
participating.

This Z evaluator will be used as part of the development of a 
model-checker for Circus, a language that
combines CSP and Z in the unifying theories of programming. After 
working in the theoretic background,
we are now at the implementation stage. Eventually, we expect this to 
become a sort of Z-Evaluator/Prover.

Best regards,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------

[CZT-Devel] Examples of CZT transformation rules

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

Dear Petra and Tim and others,

Here is an updated draft of my proposal for implementing transformation
rules (and eventually a simple theorem prover) within CZT.

You don't need to read the whole document, but
I've put more examples in (Section 3), for unfolding schema expressions,
and would like to see what you think of  them.  Does this look a nice
way of implementing schema unfolding?  

I've also updated the syntax of the proposal (Section 2), which
may interest parsing people.

Rationale:
The whole area of unfolding schema constructs is the bottleneck
in developing new CZT tools at the moment.  Virtually all Z tools
want to transform schemas etc. so need an unfolded version of them.
So we either need to implement rules like these, or hand-code schema
unfolding in Java.  If possible, I prefer the rule approach, because
*  it will allow us to prove the rules correct (not possible for Java code)
* it has many other uses (other kinds of unfolding)
* and (most importantly) it records the design of the rules at a higher
    and more readable level than Java code would.

TODO: more comparison of this proposal with CADiZ tactics
and with the rules of the Z_C and V logics for Z.

Comments?
Mark.

[CZT-Devel] Additional Object-Z.xsd changes

[Tim M. <ti...@cs...>]

Hi again,

Sorry to bother everyone with a second email, but I have made addition 
changes to the Object XML schema. The new changes are made to the 
operation expression hierarchy:

- Remove OperationBoxExpr. This seems unnecessary. It is used only as an 
abstract superclass of OperationBox and OperationExpr, which are unrelated.
- Renamed OperationBox to OpText. OpText has been changed to be more 
like a schema text (i.e. the text of an operation). So it is now made up 
of a delta list and a schema text.
- Removed MainOpExpr, and modified DistOpExpr to have SchText and Expr 
to be consistent with quantifier expressions in the Z XML schema.
- Renamed Operation* to Op* for internal consistency.
- BasicOpExpr is renamed to AnonOpExpr and now has an OpText, instead of 
a MainOpExpr.
- Replaced all List Pred with just Pred to be consistent with the Z XML 
schema.

These changes do have a small effect on the TCOZ schema, which I will 
also update, but they do not change the hierarchy at all.

Comments welcome. If nobody objects then I will commit these changes.

Cheers,
Tim

Tim Miller wrote:

 > Hi everyone,
 >
 > In fixing up the CZT Object-Z parser, I have noticed several items 
that needed addressing in Object-Z XML schema. Attached is a new version 
of the schema. There are several major changes, and any feedback would 
be welcome. The changes are:
 >
 > - Added a ClassUnionExpr for class unions.
 > - Added a ClassType.
 > - Removed PromotedAttrExpr. This is not needed/possible because it 
represents a dereference a.b, which cannot be distinguished from a 
schema binding selection in the parser, so we can treat them both a 
selection expressions.
 > - Removed SelfExpr. This is not really necessary - we can just treat 
a reference expr to the implicit state variable "self". This will 
simplify any tools that use these classes.
 > - Removed PromotedInitPred. As with self, we can treat "a.Init" as a 
selection expr.
 >
 > Then, I've also changed the following to be consistent with similar 
constructs in Z.xsd:
 > In InheritedClass
 > - Replaced ActualParameters with List Expr.
 > - Replaced RenameList with List NameNamePair.
 >
 > In ClassPara
 > - Replaced SecondaryAttributes with List Decl
 > - Replaced FormalParameters with List DeclName
 > - Replaced LocalDef with List Para
 > - Replaced RefNameList with List RefName
 >
 > Any comments/objections?
 >
 > Cheers,
 > Tim

Re: [CZT-Devel] Object-Z.xsd changes

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

Tim Miller wrote:

> In fixing up the CZT Object-Z parser, I have noticed several items 
> that needed addressing in Object-Z XML schema. Attached is a new 
> version of the schema. There are several major changes, and any 
> feedback would be welcome. The changes are:
>
> - Added a ClassUnionExpr for class unions.
> - Added a ClassType.
> - Removed PromotedAttrExpr. This is not needed/possible because it 
> represents a dereference a.b, which cannot be distinguished from a 
> schema binding selection in the parser, so we can treat them both a 
> selection expressions.
> - Removed SelfExpr. This is not really necessary - we can just treat a 
> reference expr to the implicit state variable "self". This will 
> simplify any tools that use these classes.
> - Removed PromotedInitPred. As with self, we can treat "a.Init" as a 
> selection expr.
>
> Then, I've also changed the following to be consistent with similar 
> constructs in Z.xsd:
> In InheritedClass
> - Replaced ActualParameters with List Expr.
> - Replaced RenameList with List NameNamePair.
>
> In ClassPara
> - Replaced SecondaryAttributes with List Decl
> - Replaced FormalParameters with List DeclName
> - Replaced LocalDef with List Para
> - Replaced RefNameList with List RefName
>
> Any comments/objections?

These changes look good to me.
They should make things more regular and simple for tools builders.

Assuming that noone objects to the changes, can you please commit
the new schema and ask Petra to use GnAST to regenerate the corejava 
classes?

Thanks!
Mark.

[CZT-Devel] Object-Z.xsd changes

[Tim M. <T.M...@cs...>]

Hi everyone,

In fixing up the CZT Object-Z parser, I have noticed several items 
that needed addressing in Object-Z XML schema. Attached is a new 
version of the schema. There are several major changes, and any 
feedback would be welcome. The changes are:

- Added a ClassUnionExpr for class unions.
- Added a ClassType.
- Removed PromotedAttrExpr. This is not needed/possible because it 
represents a dereference a.b, which cannot be distinguished from a 
schema binding selection in the parser, so we can treat them both 
a selection expressions.
- Removed SelfExpr. This is not really necessary - we can just 
treat a reference expr to the implicit state variable "self". This 
will simplify any tools that use these classes.
- Removed PromotedInitPred. As with self, we can treat "a.Init" as 
a selection expr.

Then, I've also changed the following to be consistent with 
similar constructs in Z.xsd:
In InheritedClass
- Replaced ActualParameters with List Expr.
- Replaced RenameList with List NameNamePair.

In ClassPara
- Replaced SecondaryAttributes with List Decl
- Replaced FormalParameters with List DeclName
- Replaced LocalDef with List Para
- Replaced RefNameList with List RefName

Any comments/objections?

Cheers,
Tim