You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}
(2) 

2004 
_{Jan}
(2) 
_{Feb}
(15) 
_{Mar}
(10) 
_{Apr}
(1) 
_{May}
(1) 
_{Jun}
(4) 
_{Jul}
(2) 
_{Aug}
(3) 
_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}
(3) 
2005 
_{Jan}
(3) 
_{Feb}
(17) 
_{Mar}
(6) 
_{Apr}
(13) 
_{May}
(17) 
_{Jun}
(53) 
_{Jul}
(36) 
_{Aug}
(29) 
_{Sep}
(17) 
_{Oct}
(21) 
_{Nov}
(37) 
_{Dec}
(25) 
2006 
_{Jan}

_{Feb}
(29) 
_{Mar}
(85) 
_{Apr}
(27) 
_{May}
(25) 
_{Jun}
(57) 
_{Jul}
(3) 
_{Aug}
(8) 
_{Sep}
(24) 
_{Oct}
(43) 
_{Nov}
(22) 
_{Dec}
(10) 
2007 
_{Jan}
(29) 
_{Feb}
(38) 
_{Mar}
(11) 
_{Apr}
(29) 
_{May}
(16) 
_{Jun}
(1) 
_{Jul}
(20) 
_{Aug}
(25) 
_{Sep}
(6) 
_{Oct}
(25) 
_{Nov}
(16) 
_{Dec}
(14) 
2008 
_{Jan}
(18) 
_{Feb}
(12) 
_{Mar}
(3) 
_{Apr}
(1) 
_{May}
(23) 
_{Jun}
(3) 
_{Jul}
(7) 
_{Aug}

_{Sep}
(16) 
_{Oct}
(27) 
_{Nov}
(16) 
_{Dec}
(7) 
2009 
_{Jan}
(1) 
_{Feb}
(12) 
_{Mar}

_{Apr}
(16) 
_{May}
(2) 
_{Jun}
(4) 
_{Jul}

_{Aug}
(4) 
_{Sep}
(7) 
_{Oct}
(12) 
_{Nov}
(8) 
_{Dec}

2010 
_{Jan}

_{Feb}

_{Mar}
(2) 
_{Apr}

_{May}

_{Jun}
(8) 
_{Jul}

_{Aug}
(11) 
_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}
(1) 
2011 
_{Jan}
(14) 
_{Feb}
(20) 
_{Mar}
(3) 
_{Apr}
(1) 
_{May}
(1) 
_{Jun}
(23) 
_{Jul}
(1) 
_{Aug}
(3) 
_{Sep}
(5) 
_{Oct}
(19) 
_{Nov}
(1) 
_{Dec}
(5) 
2012 
_{Jan}
(19) 
_{Feb}
(4) 
_{Mar}

_{Apr}
(1) 
_{May}
(2) 
_{Jun}
(7) 
_{Jul}
(33) 
_{Aug}
(3) 
_{Sep}
(3) 
_{Oct}

_{Nov}

_{Dec}

2013 
_{Jan}

_{Feb}

_{Mar}
(3) 
_{Apr}
(48) 
_{May}
(1) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2014 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}

2015 
_{Jan}
(1) 
_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(15) 
_{Sep}

_{Oct}

_{Nov}

_{Dec}

2016 
_{Jan}

_{Feb}
(1) 
_{Mar}
(1) 
_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}
(1) 
_{Dec}

S  M  T  W  T  F  S 



1
(3) 
2
(2) 
3
(2) 
4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30




From: Tim Miller <tmill@cs...>  20090903 03:53:26

Hi Pablo, You wrote: > My problem is that \{2\} has type PSTATUS > Expression: \{ 2 \} > Type: \arithmos > Expected type: PSTATUS > The problem is that the typechecker uses the type annotations on set expressions to apply the type rules. For example, the predicate: {1} = {} = {{1}} is illtyped. The typechecker does a first pass over the predicate to infer all of the types. The second pass will then check that the equality {1} = {} is well typed, and then {} = {{1}} is also well typed. A small third pass checks that all set expressions and name references have had their types fully determined. During the second pass, the typechecker uses the type annotation to determine the type of {}, because it cannot be determined from the expression itself. Now, for simplicity, the second pass is actually the same as the first pass (the rules are applied both times), but the second pass will contain ALL of the type information. In the case of set expressions, the type information is read from the annotations of the "inner" expressions. For the empty set, there are no inner expressions, so the type cannot be determine from the expression itself... it must be unified from another type. In your case, you are changing the underlying expression, so the type changes, but the type annotation remains. It seems that you will have to remove the type annotations and retypecheck unfortunately. You only need to remove SOME annotations though: definitely set expressions, probably names (I haven't really thought this through), and possibly theta expressions (although I don't think so). The only other solution I can think of is to modify the typechecker (the first block of visitSetExpr in the ExprChecker class) so that it only reads the type of the inner expressions from the type annotations if it can not determine the type (the result of typechecking the inner expressions is a variable type); that is, if it is an empty set, or a set of elements whose types have not yet been determined. This will solve your problem for most cases, but it will still remain for the empty set etc. (I think?). Alternatively, you could modified the typechecker to ignore type annotations on the first pass of a predicate, which will replace all old annotations with new ones. Tim 
From: Tim Miller <tmiller@un...>  20090903 03:47:22

Hi Pablo, You wrote: > My problem is that \{2\} has type PSTATUS > Expression: \{ 2 \} > Type: \arithmos > Expected type: PSTATUS > > I solved the problem (efficiently, I think) with operators but not with > set extensions, sequences, etc. > The problem is that the typechecker uses the type annotations on set expressions to apply the type rules. For example, the predicate: {1} = {} = {{1}} is illtyped. The typechecker does a first pass over the predicate to infer all of the types. The second pass will then check that the equality {1} = {} is well typed, and then {} = {{1}} is also well typed. A small third pass checks that all set expressions and name references have had their types fully determined. During the second pass, the typechecker uses the type annotation to determine the type of {}, because it cannot be determined from the expression itself. Now, for simplicity, the second pass is actually the same as the first pass (the rules are applied both times), but the second pass will contain ALL of the type information. In the case of set expressions, the type information is read from the annotations of the "inner" expressions. For the empty set, there are no inner expressions, so the type cannot be determine from the expression itself... it must be unified from another type. In your case, you are changing the underlying expression, so the type changes, but the type annotation remains. It seems that you will have to remove the type annotations and retypecheck unfortunately. You only need to remove SOME annotations though: definitely set expressions, probably names (I haven't really thought this through), and possibly theta expressions (although I don't think so). The only other solution I can think of is to modify the typechecker (the first block of visitSetExpr in the ExprChecker class) so that it only reads the type of the inner expressions from the type annotations if it can not determine the type (the result of typechecking the inner expressions is a variable type); that is, if it is an empty set, or a set of elements whose types have not yet been determined. This will solve your problem for most cases, but it will still remain for the empty set etc. (I think?). Alternatively, you could modified the typechecker to ignore type annotations on the first pass of a predicate, which will replace all old annotations with new ones. Tim 
From: <palbertengo@fl...>  20090902 14:35:56

Thanks Tim and Leo for your answers. Tim wrote: This causes your problem because the AST predicate that is being typechecked is actually: 0 \in \dom ( \emptyset \nrres[PID,PSTATUS] \{ 2 \}) . Not really.I solved this situation in this part of the code: if(isReserved){ // Is an operator ZExprList zExprList = refExpr.getZExprList(); for(int i=0;i<zExprList.size();i++) { Expr expr = zExprList.get(i); if(expr instanceof RefExpr) { ZName zName = zFactory.createZName(UtilSymbols.naturalSymbol(), zFactory.createZStrokeList(),"nat"); RefExpr rExpr = zFactory.createRefExpr(zName, zFactory.createZExprList(),false,false); zExprList.set(i, rExpr); } else zExprList.set(i, (Expr)expr.accept(this)); } My problem is that \{2\} has type PSTATUS Expression: \{ 2 \} Type: \arithmos Expected type: PSTATUS I solved the problem (efficiently, I think) with operators but not with set extensions, sequences, etc. My solution for this last group was remove the TypeAnn and delegate the job to the typechecker. The problem (I think) is that the solution is inefficient because I need to evaluate thousands of predicates. Any ideas of another solution? Cheers, Pablo 
From: Leo Freitas <leo@cs...>  20090902 10:50:00

Hi Pablo, Tim's explanation of the type system is pretty accurate and nails the problem down well. Yet, I couldn't help thinking you might actually be asking the wrong question as your theorem. For instance, regardless of types x \in \dom( \emptyset \nrres S) is always going to be false. Also, based on your previous email, and as Tim has said, if you want to "transform/extract" 0 \in \dom( \emptyset \nrres \{ 2 \} ) from which the original type was PID \cross PSTATUS, you will have to somehow relate \arithmos with these given types. And such type relationships are akin to data refinement. So, perhaps what you need is a refinement calculator, and there are some available, where you transform, now formally, your specification data types. *I don't think it is wise to hard code a solution* as yours in the typechecker or any other tool, given the fact there is a whole theory and tools available for that activity, unless you've come up with some specialised refinement theory or if your problem is not quite a refinement one. I mean, could you shed some light on what is what you are trying to achieve exactly? Perhaps with that, by seeing the bigger picture, we could comment better about possible solutions. Best, Leo Tim Miller wrote: > Hi Pablo, > > palbertengo@... wrote: >> The errors are of this kind: >> >> 0 \in \dom ( \emptyset \nrres \{ 2 \} ) \\ >> \emptyset \neq \{ \} \\ >> \{ 0 \} = \dom \emptyset >> ******************* >> The predicate did not pass the typechecking stage: >> ["/home/palbertengo/Desktop/Poda/TeoremaFastest2/schedulerft.tex", line >> 144: Argument to function application has unexpected type >> Expression: ( \emptyset \nrres \{ 2 \} ) >> Expected type: \power ( PID \cross PSTATUS ) \cross \power PSTATUS >> Actual type: \power ( \arithmos \cross \arithmos ) \cross \power >> \arithmos] >> > Ok, so I can see what the problem is. PID and PSTATUS are given sets, so > they are incompatible with the given set \arithmos. While the expression > 0 \in \dom ( \emptyset \nrres \{ 2 \}) is type correct, the problem with > replacing the PID/PSTATUS expressions with natural numbers is that the Z > standard specifies that the typechecker should replace all implicit > generic type instantiations with explicit instantiations. > > What this means is that the typechecker will actually modify the term in > the AST from > > 0 \in \dom ( \emptyset \nrres \{ 2 \} ) > > to > > 0 \in \dom ( \emptyset \nrres[\arithmos,\arithmos] \{ 2 \} ) . > > The name \nrres is declared as a generic name (\nrres[X,Y]). Any use of > that name must instantiate the parameters X and Y. In the first > predicate above, these are instantiated implicitly; that is, the > typechecker infers the types from the types of expressions that are > applied to the relation. In the second predicate above, the parameters > are explicitly instantiated by providing the set they come from. The > typechecker will replace any implicit instantiations with explicit > instantiations. > > This causes your problem because the AST predicate that is being > typechecked is actually: > > 0 \in \dom ( \emptyset \nrres[PID,PSTATUS] \{ 2 \} ) . > > So, the type of \nrres is '\power ( PID \cross PSTATUS ) \cross \power > PSTATUS', while the arguments are both \arithmos. > > I can think of no way around this other than for you to modify the > typechecker such that it has an option to not add the explicit > instantiations. Instantiations are added in the class > net.sourceforce.czt.typecheck.z.PostChecker, in the visitRefExpr method. > The block: > > Expr expr = (Expr) type.accept(carrierSet()); > assert expr != null; > exprs.add(expr); > > add the expressions. It shouldn't be too difficult to modify your local > copy to not add these, or to add a switch to the typechecker that gives > the user an option not to add these. > > Alternatively, if this is just a oneoff specification for which you are > doing this, you can simply declared PID and STATUS as subsets of > \arithmos, but I suspect you are after a more general solution. > > I hope this goes some way to helping you. > > Cheers, > Tim > >  > Let Crystal Reports handle the reporting  Free Crystal Reports 2008 30Day > trial. Simplify your report design, integration and deployment  and focus on > what you do best, core application coding. Discover what's new with > Crystal Reports now. http://p.sf.net/sfu/bobjjuly > _______________________________________________ > CZTDevel mailing list > CZTDevel@... > https://lists.sourceforge.net/lists/listinfo/cztdevel 
From: Tim Miller <tmill@cs...>  20090901 23:39:03

Hi Pablo, palbertengo@... wrote: > The errors are of this kind: > > 0 \in \dom ( \emptyset \nrres \{ 2 \} ) \\ > \emptyset \neq \{ \} \\ > \{ 0 \} = \dom \emptyset > ******************* > The predicate did not pass the typechecking stage: > ["/home/palbertengo/Desktop/Poda/TeoremaFastest2/schedulerft.tex", line > 144: Argument to function application has unexpected type > Expression: ( \emptyset \nrres \{ 2 \} ) > Expected type: \power ( PID \cross PSTATUS ) \cross \power PSTATUS > Actual type: \power ( \arithmos \cross \arithmos ) \cross \power > \arithmos] > Ok, so I can see what the problem is. PID and PSTATUS are given sets, so they are incompatible with the given set \arithmos. While the expression 0 \in \dom ( \emptyset \nrres \{ 2 \}) is type correct, the problem with replacing the PID/PSTATUS expressions with natural numbers is that the Z standard specifies that the typechecker should replace all implicit generic type instantiations with explicit instantiations. What this means is that the typechecker will actually modify the term in the AST from 0 \in \dom ( \emptyset \nrres \{ 2 \} ) to 0 \in \dom ( \emptyset \nrres[\arithmos,\arithmos] \{ 2 \} ) . The name \nrres is declared as a generic name (\nrres[X,Y]). Any use of that name must instantiate the parameters X and Y. In the first predicate above, these are instantiated implicitly; that is, the typechecker infers the types from the types of expressions that are applied to the relation. In the second predicate above, the parameters are explicitly instantiated by providing the set they come from. The typechecker will replace any implicit instantiations with explicit instantiations. This causes your problem because the AST predicate that is being typechecked is actually: 0 \in \dom ( \emptyset \nrres[PID,PSTATUS] \{ 2 \} ) . So, the type of \nrres is '\power ( PID \cross PSTATUS ) \cross \power PSTATUS', while the arguments are both \arithmos. I can think of no way around this other than for you to modify the typechecker such that it has an option to not add the explicit instantiations. Instantiations are added in the class net.sourceforce.czt.typecheck.z.PostChecker, in the visitRefExpr method. The block: Expr expr = (Expr) type.accept(carrierSet()); assert expr != null; exprs.add(expr); add the expressions. It shouldn't be too difficult to modify your local copy to not add these, or to add a switch to the typechecker that gives the user an option not to add these. Alternatively, if this is just a oneoff specification for which you are doing this, you can simply declared PID and STATUS as subsets of \arithmos, but I suspect you are after a more general solution. I hope this goes some way to helping you. Cheers, Tim 
From: <palbertengo@fl...>  20090901 14:34:18

Quoting Tim Miller <tmill@...>: > Hi Pablo, > > You wrote: >> I load an specification, typechect it successfully and then I need >> to replace some terms of the a predicate for natural numbers. >> Finally, type check this predicate and deliver it to the evaluator >> of ZLive. >> For example, from the schema >> >> \begin{schema}{X} >> procs: PID \pfun PSTATUS \\ >> p?:PID \\ >> \where >> p? \notin \dom procs >> \end{schema} >> >> I extract the predicate and obtain >> >> 0 \notin \dom \{1,2\} >> > So, as I understand it, you are directly manipulating the AST in > memory, rather than the latex source, right? Yes, you are right >> My problem was that the new predicate not pass the typechecking >> stage in some cases. >> I resolve this problem removing the TypeAnn from some expressions, >> but now I loss a lot of efficiency because I do this operations a >> thousand of times. >> There is another way to resolve my problem? >> > Can you give an example of this (including the error that you get), and > outline what you are doing? Specifically, if you are changing the AST, > are you leaving the type annotations of the expressions that are being > remove? > > Tim The errors are of this kind: 0 \in \dom ( \emptyset \nrres \{ 2 \} ) \\ \emptyset \neq \{ \} \\ \{ 0 \} = \dom \emptyset ******************* The predicate did not pass the typechecking stage: ["/home/palbertengo/Desktop/Poda/TeoremaFastest2/schedulerft.tex", line 144: Argument to function application has unexpected type Expression: ( \emptyset \nrres \{ 2 \} ) Expected type: \power ( PID \cross PSTATUS ) \cross \power PSTATUS Actual type: \power ( \arithmos \cross \arithmos ) \cross \power \arithmos] I'm using the next visitor to transform the predicate: public Term visitTerm(Term term){ //////////////////////////////////////////////////////////// NEWCODE TypeAnn s = term.getAnn(TypeAnn.class); if(s!=null) { Type type = s.getType(); boolean b = term.getAnns().remove(s); } //////////////////////////////////////////////////////////// return VisitorUtils.visitTerm(this, term, false); } public Term visitRefExpr(RefExpr refExpr){ String refExprStr = refExpr.getZName().toString(); // If refExpr corresponds to a reserved Z word, we return refExpr. boolean isReserved = false; for(int i=0; i< UtilSymbols.getNumOfSymbols();i++){ if(refExprStr.equals(UtilSymbols.getSymbol(i))) isReserved = true; } if(isReserved){ return refExpr; //////////////////////////////////////////////////////////// NEWCODE ZExprList zExprList = refExpr.getZExprList(); for(int i=0;i<zExprList.size();i++) { Expr expr = zExprList.get(i); if(expr instanceof RefExpr) { ZName zName = zFactory.createZName(UtilSymbols.naturalSymbol(), zFactory.createZStrokeList(),"nat"); RefExpr rExpr = zFactory.createRefExpr(zName, zFactory.createZExprList(),false,false); zExprList.set(i, rExpr); } else zExprList.set(i, (Expr)expr.accept(this)); } return refExpr; //////////////////////////////////////////////////////////// } //System.out.println(" > NO"); // If this term is contained in a set comprehension with a declared variable whose // name is equal to this refExpr, we return refExpr for(int i=0; i<additionalReservedWords.size(); i++){ if(refExprStr.equals(additionalReservedWords.get(i))){ return refExpr; } } // If refExpr corresponds to a String contained in the refNumExprMap, we return // a clone of the instance of NumExpr associated to it. NumExpr numExpr = refNumExprMap.get(refExprStr); if(numExpr != null){ return (NumExpr) numExpr.accept(new CZTCloner()); } // Otherwise, we create a new instance of NumExpr, numExpr, with the value of nextInt // (which is incremented afterwards) and we add to the map refNumExprMap the pair // (refExpr, numExpr) ZFactory zFactory = new ZFactoryImpl(); ZNumeral zNumeral = zFactory.createZNumeral(BigInteger.valueOf(nextInt++)); numExpr = zFactory.createNumExpr(zNumeral); refNumExprMap.put(refExprStr,numExpr); return numExpr; } public Term visitSetCompExpr(SetCompExpr setCompExpr){ // We save the list of additional reserved words List<String> originalList = new ArrayList<String>(); for(int i=0; i<additionalReservedWords.size(); i++){ originalList.add(additionalReservedWords.get(i)); } // We add the variables declared in the SetCompExpr to the list of additional // reserved words, in order not to replace their ocurrences. ZSchText zSchText = setCompExpr.getZSchText(); DeclList declList = zSchText.getDeclList(); if(declList instanceof ZDeclList){ ZDeclList zDeclList = (ZDeclList)declList; for(int j=0; j< zDeclList.size(); j++){ Decl decl = zDeclList.get(j); if(decl instanceof VarDecl){ VarDecl varDecl = (VarDecl) decl; NameList nameList = varDecl.getName(); if (nameList instanceof ZNameListImpl) { ZNameListImpl zNameListImpl = (ZNameListImpl) nameList; for(int i=0; i < zNameListImpl.size(); i++){ String varName = zNameListImpl.get(i).toString(); additionalReservedWords.add(varName); } } } } } TextUI textUI = new TextUI(UniqueZLive.getInstance(), new PrintWriter(System.out, true)); // We replace the alphanumeric constants of the SetCompExpr recursively, without // replacing the variables declared in the SetCompExpr setCompExpr.setSchText((ZSchText) zSchText.accept(this)) ; Expr expr = setCompExpr.getExpr(); setCompExpr.setExpr((Expr) expr.accept(this)); // We restore the list of additional reserved words additionalReservedWords = originalList; return setCompExpr; } With the modifications in NEWCODE there is no more errors in the typechecking stage, but the performance of the program worsen considerably. Pablo 
From: Tim Miller <tmill@cs...>  20090901 04:41:05

Hi Pablo, You wrote: > I load an specification, typechect it successfully and then I need to > replace some terms of the a predicate for natural numbers. Finally, > type check this predicate and deliver it to the evaluator of ZLive. > For example, from the schema > > \begin{schema}{X} > procs: PID \pfun PSTATUS \\ > p?:PID \\ > \where > p? \notin \dom procs > \end{schema} > > I extract the predicate and obtain > > 0 \notin \dom \{1,2\} > So, as I understand it, you are directly manipulating the AST in memory, rather than the latex source, right? > My problem was that the new predicate not pass the typechecking stage > in some cases. > I resolve this problem removing the TypeAnn from some expressions, but > now I loss a lot of efficiency because I do this operations a thousand > of times. > There is another way to resolve my problem? > Can you give an example of this (including the error that you get), and outline what you are doing? Specifically, if you are changing the AST, are you leaving the type annotations of the expressions that are being remove? Tim 