#68 Error in generated PO for Library example

[Peter Gorm Larsen]

For
ExeFind: String * Library -> (set of BookId)
ExeFind(s,l) ==
{bid | bid in set dom l.books @ s in set {l.books(bid).title, l.books(bid).author}}
pre card({bid | bid in set dom l.books @ s in set {l.books(bid).title, l.books(bid).author}}) > 0

we get PO's generated that are syntactically wrong...

[Luis Diogo Couto]

In overture, the record (l.books) is a AFieldExp.
In compass, it's AUnresolvedPathExp which is printed differently.

The toString method has been updated to print it correctly [a7e52a] but it's possible that these UnresolvedPaths need to be fixed.

Also, the invariantDefinition (_invDef) is not being set for the Type Definition. This causes any POs for the type invariant to not be generated.

[Claus B. Nielsen]

Fix added to [ecd1e0fa07a4942bf6b4f15a8389045525338da0]

Needs to confirmed by POG

[Luis Diogo Couto]

Fix was reverted [2a04c2].

The Invariant Definition is still not set.

[Luis Diogo Couto]

The _invariantDefinition can now be set.

(the fix was reverted since it used a removed assistant but it has been replaced by the visitor now).

Unfortunately the invDef function is not typechecked which causes the pog to crash on null pointers when it tries to process the invariant.

[Luis Diogo Couto]

Invariant definition set but not typechecked [a51483].

This will cause the POG to crash on any models that contain types with invariants.

PS: I tried uncommenting and it does indeed fail several tests.

[Claus B. Nielsen]

Type invariants are now typechecked.

Needs to be confirmed in pog.

[67120f10fac427c5dd238fcd8e2e2e0555850cc4]

[Claus B. Nielsen]

Commit [c330a2f6b35207875272290506484a520f0312ba] removes fix in[67120f10fac427c5dd238fcd8e2e2e0555850cc4] as it cause issues in some situations.

[Claus B. Nielsen]

Type invariants are now typechecked.

Needs to be confirmed in pog.

[5bf55434062674fb6bd84b948ef3d96a36e249fc]

[Luis Diogo Couto]

Close but no cigar :P

The invariant definition is being created with a null name. This causes a crash in the pog.

I noticed the lines setting the name (314-315 in TCDeclAndDefVisitor.caseAClassInvariantDefinition(...) )have been commented out.

Any reason for this?

[Claus B. Nielsen]

Cannot reproduce. The invariant definition is set to "inv_Library".

[Claus B. Nielsen]

However the name of the state invariant is not set:

in line library.cml
library: Library := mk_Library({|->},{|->},{|->})
booksP : set of BookId := {}
inv
(dom(library.borrowed) = dom(library.users)) and
(rng(library.borrowed) subset dom(library.books))

Should this be set by the parser? Or what name should it have?

[Luis Diogo Couto]

You're correct on the state invariant. Sorry for not giving the right info. On Overture this is name looks to be set by the TC during the dreaded Implicit Definitions run.

But there's another (related) null name that's problematic and is the cause of the current pog crash: the process state has null name. It uses the Overture AStateDefinition node which has a name field so we need one here or we need a new node.

I think we should come up with a naming convention for Process stuff. Maybe the parser should set the process state name ("ProcessNamestate"?) and then we set the Invariant name based on that?

Joey, any thoughts?