czt-users — For end-users of the CZT tools

Re: [CZT-Users] typchecking oz error mesages + convert oz to java/c++

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

Hi Janine,

> I am a beginner in OZ and the CZT eclipse plugin. I am writing an
> Object-Z specification in latex, but the typchecker reports some errors.
> Could someone please explain me the error messages?
>
The CZT tools (including the Object-Z ones) are based on the Z standard. 
Much of the Object-Z literature was written prior to the Z standard, so 
there are some catches that you'll have to be aware of.

The errors you see are:

- There is no "\real" set in standard Z. You can create one using:

%%Zword \real real

\begin{axdef}
   \real : \power \arithmos
\end{axdef}

  The first line tells the parser some stuff, and the paragraph below 
declares \real as a power set of 'arithmos' -- the base numbers in 
standard Z.

- The problem with the 'colour' variable is that all paragraphs in an 
Object-Z specification must be declared as standard Z paragraphs. So 
you'll need to use an axdef for that the same way that you did for the 
variable 'perim'.

Fixing these results in another problem: you'll need a '\where' symbol 
between the line that declares dx? and dy?, and the predicate that uses 
them.

> Am I right that the CTZ Tools are not able to convert the OZ code to
> Java/C++ ? If thats the case, could you point me to a tool or lib that
> is able to accomplish that task? I not only need to typecheck my OZ code
> but also have to convert it to C++ code/classes.
>
You're right that CZT doesn't do this. I've not heard of a tool that 
does, and in any case, the conversion would be highly restricted because 
Object-Z is undecidable.

I hope this helps.

Regards,
Tim

[CZT-Users] typchecking oz error mesages + convert oz to java/c++

[Janine S. <ma...@ja...>]

Hello

I am a beginner in OZ and the CZT eclipse plugin. I am writing an Object-Z specification in latex, but the typchecker reports some errors. 
Could someone please explain me the error messages?

\documentclass[11pt]{article}
\usepackage{oz}

\begin{document}


\begin{zsection}

\SECTION Shape \parents oz\_toolkit, standard\_toolkit

\end{zsection}


\begin{class}{Shape[COLOUR]}

\also

colour: COLOUR \\

\begin{axdef}

perim: \real

\where

perim > 0

\end{axdef} \\

\begin{classcom}

This class has 2 constants

$colour$ and $perim$.

\end{classcom} \\

\begin{state}

x, y: \real

\end{state} \\

\begin{init}

x = y = 0

\end{init} \\

\begin{op}{Translate}

\Delta (x,y) \\

dx?, dy?: \real

x' = x + dx? \\

y' = y + dy?

\end{op}

\end{class}

\end{document}



errors:



line 10 column 0 in : Syntax error at symbol colour

line 12 column 7 in : Unknown latex command \real

line 21 column 6 in : Unknown latex command \real

line 28 column 10 in : Unknown latex command \real





Am I right that the CTZ Tools are not able to convert the OZ code to Java/C++ ? If thats the case, could you point me to a tool or lib that is able to accomplish that task? I not only need to typecheck my OZ code but also have to convert it to C++ code/classes.





Thanks a lot for helping!





Kind regards, 

Janine

[CZT-Users] CZT Tools Install and execute from c++

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

Hello,

I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.

First of all i want to install CZT on my PC.

I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached

[INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]
[INFO] CZT Z VCG ......................................... SKIPPED
[INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED
[INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED
[INFO] CZT Z/Eves Integration ............................ SKIPPED
....


So maybe i have to use any other mirror to download archives that are required during installation?
I had tried all mirrors that are in MAVEN website - 

http://maven.apache.org/guides/mini/guide-mirror-settings.html

But this does not solve the problem, the installation does not finish.

And one more problem, can i after the installation animate simple Z specifications from c++ code?

If yes then please somebody replay me how can i do that?

Thank you very much,
Urmas Repinski.
 		 	   		  

[CZT-Users] Z Word Tools Release 3.0

[Anthony H. <an...@an...>]

I’m pleased to announce that version 3 of the Z Word Tools is now available from Sourceforge (http://sourceforge.net/projects/zwordtools) . Z Word tools allow you to write Z specifications in Microsoft Word and check them with fuzz or CZT. They also provide indexing, cross referencing and diagramming of your specification.

 

Version 3.0 has greatly improved keyboard handling: it is faster, non-English keyboards are handled correctly, typing works in any Word window and all settings such as overtype and word selection work correctly. 

 

Version 3 works with all Windows versions of Word from Word 2000 to Word 2010. 

I’d like to thank Abd Allah Diab for patient and skilful help with testing and fixing the Word 2010 x64 version. 

 

I am always pleased to hear about any use of the tools, and of course I’m happy to answer any questions or deal with any problems.

 

Anthony

 

Anthony Hall

 

22 Hayward Road

Oxford OX2 8LW

UK

 

+44 (0) 7779 255147

an...@an...

www.anthonyhall.org

 

 

Re: [CZT-Users] Logical operator ambiguity considered harmful

[Rob A. <rd...@le...>]

Ian,

Thanks - I was having a brainstorm. I note one oddity with the precedences. If you work at it, both ways of putting the brackets in something of the form %mu x: X | A /\ B can be type correct. The precedences give you the predicate conjunction (%mu x : X | A) /\ B, whereas I would have expected %mu x : X | (A /\ B). As Phil Clayton said on another forum, any reasonable Z style guide would strongly encourage people to bracket these weird cases. In retrospect, I wish the standard had been more restrictive about brackets. Having worked a lot with a large multi-author Z spec over the last few years, misplaced brackets are one of the most common causes of error.

Regards,

Rob.

On 19 Jul 2011, at 11:02, Ian Toyn wrote:

> Rob Arthan writes about parsing the following predicate.
> 
> {} = %lambda x: %Z @ [y: %Z | x < y] \/ [y:%Z  | y < x]
> 
> ISO Z assigns precedences to operators.
> Function construction binds tighter than relation operator application,
> which binds tighter than disjunction (whether predicate or expression).
> Those precedences have the effect of requiring the parse indicated below by parentheses.
> 
> ({} = (%lambda x: %Z @ [y: %Z | x < y])) \/ [y:%Z  | y < x]
> 
> Only then is any ambiguity in the use of logical operations considered.
> Since the left disjunct is a predicate, this disjunction is a predicate.
> 
> CZT (and also CADiZ) find the parse described above.
> 
> Does that work-around the issue, or did I miss something?
> 
> Regards,
> Ian
> 
> 
> ------------------------------------------------------------------------------
> Magic Quadrant for Content-Aware Data Loss Prevention
> Research study explores the data loss prevention market. Includes in-depth
> analysis on the changes within the DLP market, and the criteria used to
> evaluate the strengths and weaknesses of these DLP solutions.
> http://www.accelacomm.com/jaw/sfnl/114/51385063/
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users

Re: [CZT-Users] Logical operator ambiguity considered harmful

[Ian T. <ian...@gm...>]

Rob Arthan writes about parsing the following predicate.

{} = %lambda x: %Z @ [y: %Z | x < y] \/ [y:%Z  | y < x]

ISO Z assigns precedences to operators.
Function construction binds tighter than relation operator application,
which binds tighter than disjunction (whether predicate or expression).
Those precedences have the effect of requiring the parse indicated below by parentheses.

({} = (%lambda x: %Z @ [y: %Z | x < y])) \/ [y:%Z  | y < x]

Only then is any ambiguity in the use of logical operations considered.
Since the left disjunct is a predicate, this disjunction is a predicate.

CZT (and also CADiZ) find the parse described above.

Does that work-around the issue, or did I miss something?

Regards,
Ian

[CZT-Users] Logical operator ambiguity considered harmful

[Rob A. <rd...@le...>]

Section 8.4 of the ISO Z standard points out that logical operators (conjunction, disjunction etc.) can be used both to form predicates and to form expressions. It goes on to claim that  the resulting ambiguity is "benign, as both interpretations have the same precedence, associativity and meaning". Unfortunately, that's only true on an unwarranted assumption about the shapes of parse trees. To see this consider the following two predicates (in e-mail syntax using (* ... *) for comments):

{} = ( %lambda x: %Z @ (  [y: %Z  | x < y] \/ [y:%Z  | y < x] ) )      (*1*)

({} = ( %lambda x: %Z @[y: %Z  | x < y] ) \/  [y:%Z  | y < x]          (*2*)

Predicate 1 has no free variables and contains a schema disjunction. Predicate 2 has both free and bound occurrences of x and y and contains a predicate disjunction.  But predicates 1 and 2 above are just two different ways of resolving the ambiguity in the following construct:

{} = %lambda x: %Z @[y: %Z  | x < y] \/ [y:%Z  | y < x]   (*3*)

According to the ISO standard this ambiguity is benign, i.e., it does not matter how we resolve the ambiguity. But this is not so, even if we ignore the difference in the free variables: as neither of the lambda abstractions can be empty, predicate 1 is false, while predicate 2 is equivalent to the assertion that y < x.

You can cook up similar examples using mu-expressions or using schema quantifications. An experiment with CZT (source at: http://dl.dropbox.com/u/34693999/ambiguity.zed8) shows that it rejects predicate 3 unless x and y are in scope, so it looks like it is taking reading 2.

The required assumption on the shapes of parse trees can be made to hold by doing what ProofPower does and imposing a restriction like the one that Spivey imposes on mu- and lambda-expressions extended to cover schema quantifications. Under this restriction, these constructs are only allowed as expressions when enclosed in brackets.

Regards,

Rob.

Re: [CZT-Users] Command -cp option for Sections.

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

Hi Ray,

Thanks a lot for the patch; I've applied it to the code in the repository.

Cheers,
Petra

[CZT-Users] Command -cp option for Sections.

[Ray R. <ray...@gm...>]

I have multiple latex files in several directories which means I need to use
the commandline -cp [path] to find the parent SECTION files.  I think there
is a bug where the file being processes is in the local directory.  The
current code fails to set the czt.path if the file argument file.getParent()
== null.  This happens when the given file argument has no associated path
information.  So ./spec.tex is ok, /a/b/c/spec.tex is ok but just spec.tex
tickles the bug which results in the -cp argument being ignored.

e.g.,

java -jar czt.jar -cp ../sections spec.tex  // fails as the -cp arg is
ignored and the czt.path is not set.

However,

java -jar czt.jar -cp ../sections ./spec.tex    // works ok with current
code.

The fix is adjusting an if's bracing so the czt.path is always set if the
variable cztpath is some parsed value from the arguments.

SVN DIFF is below from a updated repository copy.

Thanks for all your hard work on CZT.

Ray


Index: ui/src/main/java/net/sourceforge/czt/ui/Main.java
===================================================================
--- ui/src/main/java/net/sourceforge/czt/ui/Main.java (revision 7414)
+++ ui/src/main/java/net/sourceforge/czt/ui/Main.java (working copy)
@@ -223,11 +223,10 @@
             cztpath = ((cztpath == null || cztpath.isEmpty()) ? fileParent
:
               (oldcztpath.isEmpty() ? (fileParent + File.pathSeparator +
cztpath) :
                 (fileParent + File.pathSeparator + oldcztpath +
File.pathSeparator + cztpath)));
-            if (cztpath != null && !cztpath.trim().isEmpty())
-            {
+  }
+  if (cztpath != null && !cztpath.trim().isEmpty()) {
                manager.setProperty("czt.path", cztpath);
             }
-          }
           boolean parsed = parse(source, manager, syntaxCheckOnly, prove,
domainCheck);
           if (parsed && output != null) {
             String dcOutput = getDCFilename(output);

-- 
The object of life is not to be on the side of the majority, but to escape
finding oneself in the ranks of the insane. - Marcus Aurelius

[CZT-Users] Z Word Tools now support ISO Standard Z

[Anthony H. <an...@an...>]

I'm pleased to announce the release of Version 2.0 of the Z Word Tools. The main new feature in this release is that you can write ISO Standard Z and typecheck your specification using a built in interface to the Community Z Tools (http://czt.sourceforge.net/) typechecker. I'm very grateful to Tim Miller, of the CZT project, for help with this. 

Of course Z Word Tools continues to support Spivey Z using fuzz and there need be no change to existing documents.

In addition there are other improvements especially for large specifications.

The new version is available at http://sourceforge.net/projects/zwordtools/ where there are full release notes.

I hope you find the new version useful. Please do let me know of any problems or comments


Anthony Hall

22 Hayward Road
Oxford OX2 8LW
UK

+44 (0) 7779 255147
an...@an...
www.anthonyhall.org

Re: [CZT-Users] CZT specification editor

[Kaiser S. <soc...@gm...>]

Thanks for your prompt reply. Also, I've had issues using the CZT Eclipse
plugin. the IDE is throwing the warning below on startup:

The activator net.sourceforge.czt.eclipse.CZTPlugin for bundle
net.sourceforge.czt.eclipse is invalid

When I go to New -> Project -> CZT -> CZT project, Eclipse complains that it
cannot open up the CZT wizard due to the following error:

The selected wizard could not be started.
  Plug-in net.sourceforge.czt.eclipse was unable to load class
net.sourceforge.czt.eclipse.wizards.NewCZTProjectWizard.
  net.sourceforge.czt.eclipse.wizards.NewCZTProjectWizard


I've also tried compiling CZT from source. Running  mvn clean install halts
with the following error:

Failed to execute goal on project maven-gnast-plugin: Could not resolve
dependencies for project
net.sourceforge.czt:maven-gnast-plugin:maven-plugin:1.5: Could not find
artifact net.sourceforge.czt:gnast:jar:1.5-SNAPSHOT

Any pointers would be greatly appreciated.

Regards,

Victor

On Tue, Jan 18, 2011 at 8:02 PM, Ray Racine <ray...@gm...> wrote:

> I use emacs with czt from the command line to check. Tried jedit but I'm
> comfortable with emacs.
>

Re: [CZT-Users] CZT specification editor

[Ray R. <ray...@gm...>]

I use emacs with czt from the command line to check. Tried jedit but I'm
comfortable with emacs.

[CZT-Users] CZT specification editor

[Kaiser S. <soc...@gm...>]

Hello all, I'm wondering if any of you use the Java CZT plugin, or just use
the rather circuitous route of using the jEdit CZT plugins to edit Z
specifications. Is the jeEdit methodology the main way you edit the CZT
specifications, or are there alternate ways to get up and running. I need a
simpler way as I'll be offering a tutorial to folks with limited Software
Development experience. I have never used the Z specification myself, so a
simpler method will also be easier on me. Thanks and please do let me know.

Regards,

Victor

Re: [CZT-Users] How to tell CZT typechecker to ignore certain Latex commands

[Nuno A. <nun...@un...>]

Thanks Tim. It works!

Cheers,
  Nuno.

On 18 Jan 2011, at 12:11, Tim Miller wrote:

> Hi Nuno,
> 
> You wrote:
>> I would like the CZT typechecker to ignore certain latex commands. Fuzz had the %%ignore directive to enable this. Is there a similar directive for the CZT typechecker?
>> 
> There is no ignore command,  but you can accomplish the same thing by adding a latex directive of the form:
> 
> %%Zword \zbreak {}
> 
> This tells the lexer to convert all \zbreak commands into nothing, so the parser will not see them. Alternatively, you can use
> 
> %%Zword \zbreak \\
> 
> which will convert all \zbreak commands into newline characters, so they can be used as whitespace.
> 
> Regards,
> Tim

Re: [CZT-Users] How to tell CZT typechecker to ignore certain Latex commands

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

Hi Nuno,

You wrote:
> I would like the CZT typechecker to ignore certain latex commands. Fuzz had the %%ignore directive to enable this. Is there a similar directive for the CZT typechecker?
>
There is no ignore command,  but you can accomplish the same thing by 
adding a latex directive of the form:

%%Zword \zbreak {}

This tells the lexer to convert all \zbreak commands into nothing, so 
the parser will not see them. Alternatively, you can use

%%Zword \zbreak \\

which will convert all \zbreak commands into newline characters, so they 
can be used as whitespace.

Regards,
Tim

[CZT-Users] How to tell CZT typechecker to ignore certain Latex commands

[Nuno A. <nun...@un...>]

Hi,

I would like the CZT typechecker to ignore certain latex commands. Fuzz had the %%ignore directive to enable this. Is there a similar directive for the CZT typechecker?


The problem is that I have a very long Z definition that goes beyond one page. I need to use the command '/zbreak' so that latex breaks the definition into two pages.

Is this possible?

Many Thanks,
   Nuno Amálio. 

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

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

Hi Weiguang Wang,

You wrote:
> When I run the command "svn update ",
> It responds after a few seconds and gets the result message :  version 7276.
> But it seems that no files have been downloaded.
> And in the toplevel pom.xml file, the
> <module>maven-sitesource-plugin</module> exists.

I am afraid I don't know what is causing your problems and how to fix
it.  Revision 7276 is the latest so that looks right to me.  But I've
deleted the module line you mentioned above so you don't seem to be
looking at the latest revision.  Try "svn -v status pom.xml"
If I do that I see "7276     7275 petramalik   pom.xml" which means
revision 7275 was the last change to pom.xml.  And if I do "svn log
pom.xml" and can see what that change that was.
Maybe just do a completely fresh checkout and start anew?

> I remembered that in the Forums of the CZT at sourceforge you have mentioned
> a svn update 
> command to get the latest version of the tool, but I can't find the Forums
> now.. Could you please tell me that command again ?

I don't know what command you are referring to.  svn update should give
you the latest version.

The forums are here:
http://sourceforge.net/projects/czt/forums
if you want to have another look yourself.

Let us know what the problem was if you figure it out.

Cheers,
Petra

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

[Weiguang W. <bi...@gm...>]

Thanks Petra

When I run the command "svn update ",
It responds after a few seconds and gets the result message :  version 7276.
But it seems that no files have been downloaded.
And in the toplevel pom.xml file, the
<module>maven-sitesource-plugin</module> exists.

I remembered that in the Forums of the CZT at sourceforge you have mentioned
a svn update 
command to get the latest version of the tool, but I can't find the Forums
now.. Could you please tell me that command again ?

Thank you.

wang

-----Original Message-----
From: Petra Malik [mailto:Pet...@ec...] 
Sent: Wednesday, November 03, 2010 9:04 PM
To: czt...@li...
Cc: Weiguang Wang
Subject: Re: Install Error of CZT and the help to derive the AST

Hi Wang,

I've installed the same versions on my linux machine (maven-3.0 and Java
1.6.0_22) and cannot reproduce your problems.  It looks to me as if you
are still using an old CZT version, which is strange since you claim to
have done an "svn update".  The failing JaxbXmlWriterReaderTest has been
fixed some weeks ago and in my recent commit I've disabled building the
maven-sitesource-plugin so the following

> [INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS
[1.402s]
> [INFO] CZT Site-Source Maven Plugin ...................... FAILURE
[2.397s]

shouldn't happen because mvn shouldn't even attempt to build the CZT
Site-Source Maven Plugin.

Please check whether you really try to build CZT with an up-to-date
version.  Maybe you've updated one directory but for building you are
using another?  Check the toplevel pom.xml file; it shouldn't contain a
line <module>maven-sitesource-plugin</module>.

Cheers,
Petra

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

[Anthony H. <an...@an...>]

Thanks Petra

>Using "mvn javadoc:javadoc" worked for me and created API documentation
>in directories target/site/apidocs/

Yes, it did do that - more or less. However, it doesn't seem quite right
because the links there are to (eg)
C:\Users\anthony\Documents\fm\z\czt\czt\target\site\session\apidocs\index.ht
ml
which doesn't exist : the actual docs seem to get built in (eg)
C:\Users\anthony\Documents\fm\z\czt\czt\session\target\site\apidocs\index.ht
ml

It's OK, I can obviously look at the individual items, but I guess something
must be set up slightly wrong?

Thank you

Anthony

Re: [CZT-Users] Maven Problem Building from SVN

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

Anthony Hall wrote:
> (However, I did get an error at first, when I ran "mvn
> -Dmaven.test.skip=true clean install"  because the Z Rules seemed to require
> the typechecker tests. When I built without skipping tests, it built OK and
> didn't actually take much longer, but perhaps there is something slightly
> wrong somewhere still?)

Yes, that's been an issue for years now but it is a problem with maven
rather than with CZT I think.

http://odoepner.wordpress.com/2009/03/04/maven-skip-tests-causes-test-jar-dependency-errors/
advises to not use -Dmaven.test.skip=true but set skipTests to true instead.

Cheers,
Petra

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

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

Dear Anthony,

You wrote:
> The CZT papers you refer to below look really useful. I didn't find these
> when searching the CZT website: I think if you pointed at them from there it
> would be really helpful to new users. (If they are on the site and I missed
> them, then apologies, but I did look!)

Yeah, the documentation is rather spread out and unstructured.  The CZT
web-site can be automatically generated from various sources but hasn't
been updated for years now (and the knowledge how to update it got lost
I guess).  I wonder whether it is worth setting up a wiki since it's
easier to keep a wiki up-to-date ... we had a wiki some time ago which
contained some useful information but it got deleted by accident.

> Also, could you please explain how to use maven to generate an up-to-date
> version of the documentation? I tried "mvn site" and it did create a site,
> but all the Javadocs links pointed to non-existent files.

Using "mvn javadoc:javadoc" worked for me and created API documentation
in directories target/site/apidocs/

Cheers,
Petra

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

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

Hi Wang,

I've installed the same versions on my linux machine (maven-3.0 and Java
1.6.0_22) and cannot reproduce your problems.  It looks to me as if you
are still using an old CZT version, which is strange since you claim to
have done an "svn update".  The failing JaxbXmlWriterReaderTest has been
fixed some weeks ago and in my recent commit I've disabled building the
maven-sitesource-plugin so the following

> [INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS [1.402s]
> [INFO] CZT Site-Source Maven Plugin ...................... FAILURE [2.397s]

shouldn't happen because mvn shouldn't even attempt to build the CZT
Site-Source Maven Plugin.

Please check whether you really try to build CZT with an up-to-date
version.  Maybe you've updated one directory but for building you are
using another?  Check the toplevel pom.xml file; it shouldn't contain a
line <module>maven-sitesource-plugin</module>.

Cheers,
Petra

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

[Weiguang W. <bi...@gm...>]

Hi Dear Petra:

Thank you very much for your replay.

My environment is: maven-3.0 , Java 1.6.0_22 and Win7 professional 32bit.  

I ran the command "svn update" , get the version 7276.
Run "mvn clean" and get the BUILD SECCESS message.
Then run "mvn install" , error occurred :

Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.006 sec
Results :
Tests in error:
  testWritingReading(net.sourceforge.czt.z.jaxb.JaxbXmlWriterReaderTest)
Tests run: 21, Failures: 0, Errors: 1, Skipped: 0
[INFO]
------------------------------------------------------------------------
[INFO] Reactor Summary:
[INFO] CZT Corejava ...................................... FAILURE
[3:28.212s]
 [INFO]
------------------------------------------------------------------------
[INFO] BUILD FAILURE
[ERROR] Failed to execute goal
org.apache.maven.plugins:maven-surefire-plugin:2.
5:test (default-test) on project corejava: There are test failures.
[ERROR]
[ERROR] Please refer to E:\CZT\cztcode\corejava\target\surefire-reports for
the
individual test results.

The report of the error message in
E:\CZT\cztcode\corejava\target\surefire-report is attached.
Please check the .txt attachment.

And then I try to skip the test procedure by adding the flag "-DskipTests".
The error is :

[INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS [1.402s]
[INFO] CZT Site-Source Maven Plugin ...................... FAILURE [2.397s]
[ERROR] Failed to execute goal
org.apache.maven.plugins:maven-plugin-plugin:2.6:
descriptor (default-descriptor) on project maven-sitesource-plugin:
Execution de
fault-descriptor of goal
org.apache.maven.plugins:maven-plugin-plugin:2.6:descri
ptor failed: An API incompatibility was encountered while executing
org.apache.m
aven.plugins:maven-plugin-plugin:2.6:descriptor:
java.lang.NoSuchMethodError: or
g.apache.maven.tools.plugin.scanner.MojoScanner.setActiveExtractors(Ljava/ut
il/S
et;)V
[ERROR] -----------------------------------------------------
[ERROR] realm =
plugin>org.apache.maven.plugins:maven-plugin-plugin:2.6-46045
6650
[ERROR] strategy =
org.codehaus.plexus.classworlds.strategy.SelfFirstStrategy
[ERROR] urls[0] =
file:/C:/Users/WGWang/.m2/repository/org/apache/maven/plugins/
maven-plugin-plugin/2.6/maven-plugin-plugin-2.6.jar
[ERROR] urls[1] =
file:/C:/Users/WGWang/.m2/repository/org/apache/maven/maven-pl
ugin-tools-ant/2.0.1/maven-plugin-tools-ant-2.0.1.jar
[ERROR] urls[2] =
file:/C:/Users/WGWang/.m2/repository/org/apache/maven/maven-pl
ugin-tools-api/2.0.1/maven-plugin-tools-api-2.0.1.jar
[ERROR] urls[3] =
file:/C:/Users/WGWang/.m2/repository/org/apache/maven/maven-pl
ugin-tools-model/2.0.1/maven-plugin-tools-model-2.0.1.jar

etc.

Hope this can explain the problem I met.
Thanks for any insight you can provide!

Wang

-----Original Message-----
From: Petra Malik [mailto:Pet...@ec...] 
Sent: Wednesday, November 03, 2010 12:01 AM
To: Weiguang Wang
Subject: Re: Install Error of CZT and the help to derive the AST

Hi Weiguang,

You wrote:
> 1)  I want to extract the AST structure from my Z specification using
> CZT, and
> 
> then do some test generation work on the AST.
> 
> Can anyone kindly offer some details or materials on how to gain that ?

You might want to have a look at Fastest, a test generation tool built
on top of CZT.
http://en.wikipedia.org/wiki/Fastest

It is described in an ICFEM'09 paper by Maximiliano Cristiá and Pablo
Rodríguez Monetti titled "Implementing and Applying the
Stocks-Carrington Framework for Model-Based Testing".

The CZT papers "CZT: A framework for Z tools" and "CZT support for Z
extensions" should give you a basic idea how to extend CZT.  Also, the
API documentation for the AST in particular should be helpful.
http://czt.sourceforge.net/corejava/apidocs/index.html
is a (probably somewhat out-of-date) on-line version but you can use
maven to generate an up-to-date version.

This mailing list is the right place to ask any specific questions
you've got.

> 2)  I have checked out the CZT trunk (revision 7273) and tried to install
it. 
> 
> After passing the “mvn clean” command, I'm getting a failure when run the
“mvn install” command:

Could you please do an "svn update" and try again?
Let us know if there are still problems (including the exact error
message and version numbers for Java and maven).

Hope this helps,
Petra

Re: [CZT-Users] Maven Problem Building from SVN

[Anthony H. <an...@an...>]

I'm sorry, please ignore the previous message. I see now that the czt.jar
file is not where I was expecting it, but in lib/czt.jar. My fault for not
reading the instructions carefully enough. Apologies

Anthony

-----Original Message-----
From: Anthony Hall [mailto:an...@an...] 
Sent: 03 November 2010 14:17
To: 'Petra Malik'; 'czt...@li...'
Subject: RE: [CZT-Users] Maven Problem Building from SVN

Dear Petra

I may have spoken too soon. Maven certainly reported success, but it didn't,
as far as I can see, build an overall czt jar file. Should it have done?  It
did build a czt-1.6-SNAPSHOT-tests.jar, but not a czt-1.6-SNAPSHOT.jar which
I expected.

Am I doing something wrong here?

Thanks again

Anthony

Re: [CZT-Users] Install Error of CZT and the help to derive the AST

[Anthony H. <an...@an...>]

Dear Petra

The CZT papers you refer to below look really useful. I didn't find these
when searching the CZT website: I think if you pointed at them from there it
would be really helpful to new users. (If they are on the site and I missed
them, then apologies, but I did look!)

Also, could you please explain how to use maven to generate an up-to-date
version of the documentation? I tried "mvn site" and it did create a site,
but all the Javadocs links pointed to non-existent files. 

Thanks for your help

Anthony

-----Original Message-----
From: Petra Malik [mailto:Pet...@ec...] 
Sent: 03 November 2010 04:03
To: czt...@li...
Subject: Re: [CZT-Users] Install Error of CZT and the help to derive the AST

Hi Weiguang,

You wrote:
>> 1)  I want to extract the AST structure from my Z specification using
>> CZT, and then do some test generation work on the AST.

You might want to have a look at Fastest, a test generation tool built
on top of CZT.
http://en.wikipedia.org/wiki/Fastest

It is described in an ICFEM'09 paper by Maximiliano Cristiá and Pablo
Rodríguez Monetti titled "Implementing and Applying the
Stocks-Carrington Framework for Model-Based Testing".

The CZT papers "CZT: A framework for Z tools" and "CZT support for Z
extensions" should give you a basic idea how to extend CZT.  Also, the
API documentation for the AST in particular should be helpful.
http://czt.sourceforge.net/corejava/apidocs/index.html
is a (probably somewhat out-of-date) on-line version but you can use
maven to generate an up-to-date version.

This mailing list is the right place to ask any specific questions
you've got.

>> 2)  I have checked out the CZT trunk (revision 7273) and tried to
install it.
>>
>> After passing the “mvn clean” command, I'm getting a failure when run
the “mvn install” command:
Could you please do an "svn update" and try again?
Let us know if there are still problems (including the exact error
message and version numbers for Java and maven).

Hope this helps,
Petra

----------------------------------------------------------------------------
--
Achieve Improved Network Security with IP and DNS Reputation.
Defend against bad network traffic, including botnets, malware, 
phishing sites, and compromised hosts - saving your company time, 
money, and embarrassment.   Learn More! 
http://p.sf.net/sfu/hpdev2dev-nov
_______________________________________________
CZT-Users mailing list
CZT...@li...
https://lists.sourceforge.net/lists/listinfo/czt-users