gsdlab / clafer Goto Github PK

In a dynamic model, enum should be desugared as follows:

enum UserRequest = stop | up | down

abstract final UserRequest
stop : UserRequest 
up : UserRequest
down : UserRequest

Clafer v0.2.27-1-2012

If a given name is found locally (among the ancestors) it should take precedence before going through descendants. References should be processed only if previous search did not yield any results.

abstract Person
    age : integer
    [ age >= 0 ]            // age should refer to Person.age, not spouse.age, nor children.age...
    xor maritalStatus
        neverMarried
        married
            [ age >= 18 ]      // here, the modeler clearly means Person.age, not spouse.age
            spouse -> Person
                [ spouse = parent.parent.parent ]     // here, the modeler means spouse.maritalStatus.married.spouse 
                [ age >= 18 ]      // here, the modeler clearly means spouse.age, not Person.age
        divorced
    children -> Person *
        [ all childAge : this.age | childAge <= parent.age  ]     // here age should refer to Person.age
        [ parent in this.parents ]     // this person should be one of the parents of his/her children
    parents -> Person 0..2   // parents may sometimes be now known
        [ parent in parent.children ]      // this person should be one of his/her parents children

Alice : Person
    [ age = 25      // meaning this.age
       spouse = Bob ]   // meaning this.maritalStatus.married.spouse
        // [ children = Carol ] should be inferred

Bob : Person
    [ age = 26
       spouse = Alice ]
        // [ children = Carol ] should be inferred

Carol : Person
    [ age = 10
       parents = Alice, Bob ]

The clafer name resolver outputs:

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
clafer: element is not unique : "age". Available paths:
c1_Person.c2_age
c1_Person.c24_children.c2_age
c1_Person.c32_parents.c2_age
c1_Person.c24_children.c24_children.c2_age
c1_Person.c24_children.c32_parents.c2_age
c1_Person.c32_parents.c24_children.c2_age
c1_Person.c32_parents.c32_parents.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c24_children.c24_children.c32_parents.c2_age
c1_Person.c24_children.c32_parents.c24_children.c2_age
c1_Person.c32_parents.c24_children.c32_parents.c2_age
c1_Person.c32_parents.c32_parents.c24_children.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c24_children.c32_parents.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c24_children.c2_age
c1_Person.c24_children.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c24_children.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c24_children.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c24_children.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c32_parents.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c32_parents.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c24_children.c6_maritalStatus.c8_married.c12_spouse.c24_children.c32_parents.c2_age
c1_Person.c24_children.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c24_children.c2_age
c1_Person.c24_children.c24_children.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c24_children.c24_children.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c24_children.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c24_children.c32_parents.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c24_children.c32_parents.c2_age
c1_Person.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c24_children.c2_age
c1_Person.c32_parents.c24_children.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c32_parents.c24_children.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c32_parents.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c32_parents.c32_parents.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c6_maritalStatus.c8_married.c12_spouse.c24_children.c32_parents.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c24_children.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c24_children.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c24_children.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c6_maritalStatus.c8_married.c12_spouse.c24_children.c2_age
c1_Person.c6_maritalStatus.c8_married.c12_spouse.c32_parents.c24_children.c6_maritalStatus.c8_married.c12_spouse.c2_age

Here's how I disambiguated the example:

abstract Person
    age : integer
        [ this >= 0 ]
    xor maritalStatus
        neverMarried
        married
            [ Person.age >= 18 ]
            spouse -> Person
                [ this.maritalStatus.married.spouse = Person ]
                [ this.age >= 18 ]
        divorced
    children -> Person *
        [ all childAge : this.age | childAge <= parent.age  ]
        [ parent in this.parents ]     // this person should be one of the parents of his/her children
    parents -> Person 2
            [ parent in this.children ]      // this person should be one of his/her parents children

The following model

abstract FeatureModel
abstract Feature
    [ parent in Feature, FeatureModel]

produces an error

Compile error at line 3 column 7...
Function 'in' cannot be performed on
TClafer {_hi = ["root"]}
in
TClafer {_hi = ["c0_Feature","c0_FeatureModel"]}

the type checker incorrectly assumes that the parent of an abstract clafer is the root.

Currently, users have to consult the release notes to figure out which language features are supported by which backend. This should be easily accessible in the CheatSheet.

For relational Clafer, we need to access relations not just sets. For example, for a model

abstract Person
   likes -> Person *
   [ some this.likes ]      // non-empty set     
   [ some this <: likes ]  // non-empty relation likes

Also, to access the relation globally, we'd like to be able to say

[ some Person <: likes ]

also, access the relation specialized to a subclafer:

abstract Student : Person

[ some Student <: likes ]

This will allow us to access relations and use them in relational expressions, such as inverse, transitive closure, etc.

Description: Recursive definitions apparently do not work in both versions, master and grammar.

How to reproduce:

create a simple example like:

abstract Person
name : string
friends -> Person *

Result: grammar: syntax error before }
Result: master: element is not unique "name"

Expected result: no compilation error.

[kgad@lt00583 /tmp/clafer]$  
 make init
cabal sandbox init --sandbox=../.clafertools-cabal-sandbox
Writing a default package environment file to
/private/tmp/clafer/cabal.sandbox.config
Using an existing sandbox located at /private/tmp/.clafertools-cabal-sandbox
# Uncomment to use Haskell LTS in the sandbox
# wget http://www.stackage.org/snapshot/lts-1.4/cabal.config
# mv cabal.config ../.clafertools-cabal-sandbox
# the constraint is there to prevent installing utf8-string-1 which conflicts with gitit, which requires utf8-string <= 0.3.8.
cabal install --only-dependencies --extra-lib-dir=/opt/local/lib --extra-include-dir=/opt/local/include/ --enable-tests --constraint="utf8-string==0.3.8"
Resolving dependencies...
cabal: Could not resolve dependencies:
trying: clafer-0.3.9 (user goal)
next goal: base (dependency of clafer-0.3.9)
rejecting: base-4.6.0.1/installed-6c3... (conflict: clafer => base>=4.7.0.1 &&
<5)
rejecting: base-4.7.0.2, 4.7.0.1, 4.7.0.0, 4.6.0.1, 4.6.0.0, 4.5.1.0, 4.5.0.0,
4.4.1.0, 4.4.0.0, 4.3.1.0, 4.3.0.0, 4.2.0.2, 4.2.0.1, 4.2.0.0, 4.1.0.0,
4.0.0.0, 3.0.3.2, 3.0.3.1 (global constraint requires installed instance)
Dependency tree exhaustively searched.

Note: when using a sandbox, all packages are required to have consistent
dependencies. Try reinstalling/unregistering the offending packages or
recreating the sandbox.
make: *** [init] Error 1

Removing the --constraint="utf8-string==0.3.8" does not solve the issue...

Clafer v0.2.6-2-2012

For the following code:

abstract A
    b *
        c ?
    [ some b1 : b | b1.c ]

The translator produces the following incorrect error:

clafer "issue17.cfr" -v -m=alloy42
issue17.cfr

Parse              Failed...

Tokens:
syntax error at line 4 before : b | b1

Hi everybody!
You are stating: "Clafer can be used with a variety of methods, such as [...] specification by example". Do you have an description/tutorial/example which explains how can I use clafer with "specification by example"/BDD/ATDD-like method? Especially I'm interested in: How do I have to extend my Gherkin-style examples by Clafer-expressions?
Regards!

This is a bug in implementation of issue #67.

For the following correct model:

abstract Object

abstract Person : Object
    abstract Hand : Object
    abstract Hook : Hand

CptHookHand : Person
    left : Hook
    right : Hand

CptHandHook : Person
    left : Hand
    right : Hook

the compiler incorrectly reports:

Refinement errors in the following places:
Improperly nested clafer 'Hook' on line 7 column 5

However, changing the model as follows:

abstract Person
    abstract Hand : Object
    abstract Hook : Hand

compiles without any errors.

Version: 0.0.3

For a model:

A
   x : integer
   [ x >= 0 ]

the resulting Alloy model is correct:

one sig c1_A
{ r_c2_x : one Int }
{ all  cl0 : this.@r_c2_x | cl0 >= 0 }

However, for a Clafer model

A
   x : integer
       [ this >= 0 ]

the resulting Alloy model is incorrect:

one sig c1_A
{ r_c2_x : one c2_x }
one sig c2_x
{ ref : one Int }
{ this >= 0 }

Reported error:

A type error has occured:
This must be an integer expression. Instead, it has the following possible type(s): {this/c2_x}

the correct code for the constraint should be

...
{ ref >= 0 }
...

Actually, x is translated incorrectly, since it does not have any children (the constraint does not require making x a signature). The code generated for the first example is correct as well.

Description: cardinality constraint does not properly when declared clafer has opt group cardinality.

How to reproduce:

abstract X
opt attrs 2
a1 -> integer
a2 -> integer

Result: error

clafer opt.cfr

Parse Failed...

Tokens:
syntax error at line 2 before { a1 -> integer

Expected result: parse should be successful. Note that it works if model is

abstract X
opt attrs 2 .. 2
a1 -> integer
a2 -> integer

Version: 0.0.3

Strange name resolution behavior and inappropriate error reporting. Two cases:

1. No error reported if the entire model is
   D.cfr

abstract A
    b ?
    [ B ]

Clearly B is undefined, and yet:

clafer3 -k D.cfr

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 2 | Abstract: 1 | Concrete: 1 | References: 0
Constraints: 1
Global scope: 1..*
All names unique: True

[Saving File]

2. However, when adding an instance a1 : A as follows

D.cfr

abstract A
    b ?
    [ B ]

a1 : A

clafer3 -k D.cfr

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0
Constraints: 1
Global scope: 1..*
All names unique: False

[Saving File]
clafer3: B not found within Just "A"SEnv {clafers = [IClafer {isAbstract = True, gcard = Just (IGCar
, interval = (0,ExIntegerAst)}), ident = "A", uid = "c1_A", super = ISuper {isOverlapping = False, s
= Just ISet, pid = "", exp = IClaferId {modName = "", sident = "clafer", isTop = True}}]}, card = J
, glCard = (0,ExIntegerAst), elements = [IEClafer (IClafer {isAbstract = False, gcard = Just (IGCard
interval = (0,ExIntegerAst)}), ident = "b", uid = "c2_b", super = ISuper {isOverlapping = False, su
= Just ISet, pid = "", exp = IClaferId {modName = "", sident = "clafer", isTop = True}}]}, card = Ju
...

and it continues printing a lot. For large models, it takes very long time to print (it never stopped for me). That is very annoying behavior.

The is a feature request to allow extending nested abstract Clafers. Consider the following example:

abstract Person
    abstract Hand

abstract Hook : Hand

CptHook : Person
    left : Hook
    right : Hand

Currently, this code would not compile as Hook is not nested under Person. It would be nice to be able to say things like

abstract  Hook : Hand

So that large models can be broken into smaller pieces. Semantically this could work if when you had an abstract Clafer with inheritance it would also inherit the relation (if it exists) between the parent and the Clafer being inherited. I.e. in our example:

Person = {(root, _Person)}
Hand = {(_Person, _Hand)}
Hook = {(_Person, _Hook)}

http://gsd.uwaterloo.ca/bugs/question/8/issue19-incorrect-expression-in-a-quantified

For the following code:

abstract AttributeToColumn
  ComplexAttributeToColumn
    atc : AttributeToColumn ?

k : AttributeToColumn 

Generated Alloy code contains a cycle between ComplexAttributeToColumn and AttributeToColumn, so that they might exist without any instance of k.

Currently (0.3.9), Clafer assumes 0 as a value for missing values, which is ok when doing addition (sum) but not multiplication (product).

For example,

a -> integer ? = 2
b -> integer ? = 3
c -> integer ? = a + b     // possible values are 0, 2, 3, or 5
d -> integer ? = a * b     // possible values are 0, 0, 0, or 6

That is because when a and b are not present, their values are assumed to be 0, which makes the result of multiplication 0 as well.

What should be the correct possible values for d: 1, 2, 3, 6 or 0, 2, 3, 6?

In general, instead of assuming a neutral element, the missing clafer should not be omitted in the formula as follows:

1. one a && one b then a + b remains as is
2. one a && no b then a + b is simplified to a
3. no a && one b then a + b is simplified to b
4. no a && no b then ?

Translate the following model

abstract Y
    y:int

Z : Y
    [y = -1]

The output

open util/integer
pred show {}
run  show for 1

abstract sig c1_Y
{ r_c2_y : one c2_y }
sig c2_y
{ ref : one Int }
{ one @r_c2_y.this }
one sig c3_Z extends c1_Y
{}
{ (this.@r_c2_y.@ref) = (1-) }

The last line shoud be -1 instead of the syntactically incorrect 1-

Added syntax

assert [ ... ]

which gets translated to Alloy as

assert assertionOnLine<n> {
  ...
}
check assertionOnLine<n> for <the same scopes as in run command>

The following model works as expected:

abstract X

A : X 
B : X 
C : X

xs ->> X * 
[ xs = A, B, C ] 

However, making X a reference

abstract X -> integer

A : X = 1
B : X = 2
C : X = 3

xs ->> X * 
[ xs = A, B, C ] 

causes the following error in Alloy:

This name is ambiguous due to multiple matches:
field this/c0_X <: ref
field this/c0_xs <: ref

The generated Alloy code is incorrect and irregular:

fact { (c0_xs.@ref) = (((c0_A.@ref) + (c0_B.@ref)) + c0_C) }

The A and B should not have @refs, so only for C is the code generated correctly.

Currently, the only way to fix it is by adding .ref as follows

[ xs = A.ref, B.ref, C.ref ] 

However, the instance produced is incorrect!

=== Instance 1 Begin ===

A = 1
B = 2
C = 3
xs$1 = C
xs$2 = B
xs$3 = A

--- Instance 1 End ---

Changing the xs to

xs ->> integer *

results in the correct instance

=== Instance 2 Begin ===

A = 1
B = 2
C = 3
xs$1 = 3
xs$2 = 2
xs$3 = 1

--- Instance 2 End ---

I suppose this has something to do with the type system.

1st Issue: I followed the instructions and tried to build the clafer project, but the following error messages appeared:

$ make
make -C tools
make[1]: Entering directory /cygdrive/d/clafer/source/clafer/tools' javac XsdCheck.java make[1]: Leaving directory/cygdrive/d/clafer/source/clafer/tools'
cabal configure
Resolving dependencies...
Configuring clafer-0.2...
cabal.exe: At least the following dependencies are missing:
cmdargs -any, executable-path -any
Makefile:17: recipe for target `build' failed
make: *** [build] Error 1

Solution: I have to manually run the two commands "cabal install cmdargs" and "cabal install executable-path" first and then the "make" command can run smoothly.

Reason: cabal install should fetch all the dependencies, but obviously it doesn't work for the fresh install. I don't know why, but I guess maybe there're some interrelationships among the dependencies that should be installed. That is to say, maybe the sequence of these dependencies written in "clafer.cabal" file matters. I don't know, but I think further test for fresh install is required.

2nd Issue: the same problem as above appears during building claferIG:
D:\clafer\source\claferIG>make
cabal configure
Resolving dependencies...
Configuring claferIG-0.0.3...
cabal.exe: At least the following dependencies are missing:
HaXml -any, haskeline -any
Makefile:75: recipe for target `build' failed
make: *** [build] Error 1

Solution: manually run "cabal install HaXml" and "cabal install haskeline" first.

Reason: the same reason as that of 1st issue.

3rd Issue: "unzip" is required for building claferIG due to the following instruction in the "Makefile" file:

unzip tools/alloy4.jar $(LIB) -d lib;

Solution: the "unzip" package should be included when installing cygwin.

In the Alloy output, the generation of group cardinality constraints is pushed down to the application site, that is, to the concrete clafers. However, doing the same for Choco looses the important information about where the group cardinality was declared.

abstract xor A       // xor declared but no constraint generated
   b
a1 : A                   // constraint generated because a1 is concrete
   c                        // the constraint applies to all children b, c, and d
   d
abstract G : A      // xor is inherited but no constraint generated
g1 : G
   e                       // the constraint applies to all children b and e

Using clafer 0.0.3

Case 1)

abstract A
x ?
y ?
[ (x => ! y) && (y => ! x) ]

produces the following error:

C:\Temp>clafer3 -k -m=clafer non-exhaustive-patterns.cfr

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0
Constraints: 1
Global scope: 1..*
All names unique: True

[Saving File]
clafer3: Intermediate\Desugarer.hs:(320,5)-(326,35): Non-exhaustive patterns in function sugarOp

Case 2)

abstract A
x ?
y ?
[ x => ! y && y => ! x ]

produces the following error:

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0
Constraints: 1
Global scope: 1..*
All names unique: True

[Saving File]
clafer3: Intermediate\Desugarer.hs:(316,18)-(328,80): Non-exhaustive patterns in case

Case 3)

abstract A
x ?
y ?
[ x => ! y
y => ! x ]

produces the following error:

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0
Constraints: 1
Global scope: 1..*
All names unique: True

[Saving File]
clafer3: Intermediate\Desugarer.hs:(320,5)-(326,35): Non-exhaustive patterns in function sugarOp

Case 4)

abstract A
x ?
y ?
[ x => ! y ]
[ y => ! x ]

is correct!

The README file, inside the src folder, states the following dependencies for compiling Clafer source code:

• ghc6
• ghc6-prof
• ghc6-doc
• cabal

Two comments:

• ghc6-doc is not actually required, unless you are a Haskell developer and needs to read its documentation

• libghc-mtl-dev was required for me, otherwise I would get the following error when running make:

  Could not find module `Control.Monad.State':
  Use -v to see a list of the files searched for.

Semantically, all top-level concrete clafers in the model are children of a synthetic root clafer. The identifier root is reserved in the same way as this or parent.

The root clafer is mostly needed for referring to top-level clafers when names are ambiguous. For example, in the following model:

test/failing/gi57.cfr

a 
    b ?
b ?
[ some a.b ]
[ some root.b ]   // error 

one can only say a.b to disambiguate. Currently (0.3.7) it is not possible to say root.b to refer to the top-level clafer. The error is

Compile error at line 7 column 13...
Name resolver: 'b' not found within paths:
in context of '"none"'

The module util/integer contains min and max functions:

/** given a set of integers, return the largest element */
fun max [es: set Int]: lone Int { es - es.^prev }

/** given a set of integers, return the smallest element */
fun min [es: set Int]: lone Int { es - es.^next }

Often when navigating deeply nested hierarchies, it is not clear what is the target a parent expression is referring to. For example,

abstract A -> integer
    abstract B -> integer
        abstract C 
abstract D
    c -> C
    [ this.c.dref.parent.parent.dref ]

Instead, we could write the constraint a bit differently using the "self-explanatory parent":

[ this.c.dref.^B.^A.dref ]

which can be read "go through the reference c to a C, then to its parent B, then to its parent A, and through the reference". For now, the statement in this notation would simply desugar to the original expression; however, additional checks are now possible (whether the resulting target of the parent is indeed what the user intended).

Version: 0.0.3
Description: instance generated by Alloy does not reflect constraints given by Clafer instance spec.

How to reproduce:

abstract Person
  name
    first : string
    last  : string
  or spokenLanguage
     english
     german
     other : string

ThomasEdison : Person
  [ first = "Thomas"
    last  = "Edison"
    english
    ! german
    other = "french"
  ]

Result: when running alloy on the produced file from clafer translator result in an instance thomasEdison with only english as spokenLanguage. Actually, Alloy produces 2 instances: 1) only english, 2) both english and other=2 (where 2 represents the string "french").

Expected result: thomasEdison instance should have english and "french" as spokenLaguages.There should be only one instance.

The help message of claferIG does not explain how to change global scope (or where to find this kind of info). Probably just a single line telling how you can get help inside IG printed in response to --help or in the IG startup messages would reduce user frustration. It took me some time to go the tools installation and to find the readme files.

X
    x:int
        y
            z
                [x > 0]

Run the above model.

clafer -o Test outputs correctly to the console

clafer Test runs into the following error

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 4 | Abstract: 0 | Concrete: 4 | References: 0
Constraints: 1
Global scope: 1..1
All names unique: True

[Saving File]
clafer: Prelude.tail: empty list

For a model

abstract ASIL -> integer
A : ASIL -> 1
B : ASIL -> 2
C : ASIL -> 3
D : ASIL -> 4

the compiler produces

...
c0_ASIL.refToUnique(Int);
c0_A.extending(c0_ASIL).refTo(Int);
c0_B.extending(c0_ASIL).refTo(Int);
c0_C.extending(c0_ASIL).refTo(Int);
c0_D.extending(c0_ASIL).refTo(Int);

whereas the correct output should be

...
c0_ASIL.refToUnique(Int);
c0_A.extending(c0_ASIL).refToUnique(1);
c0_B.extending(c0_ASIL).refToUnique(2);
c0_C.extending(c0_ASIL).refToUnique(3);
c0_D.extending(c0_ASIL).refToUnique(4);

Using compiler v. 0.0.3

Getting parse errors when using + and * cardinalities. For example,

abstract C

abstract A
b -> C *
c -> C +

Parse Failed...

Tokens:
syntax error at line 5 before -> C + }

+, *, and ? get parsed correctly when no references, e.g.,

abstract a
b ?
c +
d *

is no problem.

abstract FunctionalArchitecture
abstract Deployment
   abstract fa -> FunctionalArchitecture

// then we write our generic power window deployment

abstract PowerWindowFAA : FunctionalArchitecture
abstract PowerWindowDpl : Deployment
   abstract fa : fa -> PowerWindowFAA

// Finally, we want to specialize it to driver power window.
// Here we have concrete architecture

System
    DriverPowerWindowFAA : PowerWindowFAA       
    DriverPowerWindowDpl : PowerWindowDpl
       // refine the type again to driver
       fa : fa -> DriverPowerWindowFAA  

Results in an incorrect error:

Compile error at line 9 column 18...
clafer "fa" cannot be defined because the name should be unique in the same namespace.
Available paths:
c0_fa
c1_fa

The clafer c1_fa should not be taken into consideration because a clafer cannot extend itself.

Version: v0.1.11-1-2012
Severity: Low

Description: the output filename is being generated with an incorrect filename.

How to reproduce: create a simple model and name it test.clafer.

Expected result: an output file named test.als

Result: a file named tes.als is produced

Consider the following incorrect model:

abstract LogicalBus : LogicalBus
    xor type
        CAN
        LIN

bus1 : LogicalBus

The compiler will output the following:

clafer -m choco debug.cfr 
All clafers: 5 | Abstract: 1 | Concrete: 4 | Reference: 0
Constraints: 0
Goals: 0

The Clafer process then hangs and does not complete. This type of inheritance should not be allowed and should throw an compile error.

Clafer v0.1.21-12-2011

Desugaring the following incorrect model

abstract A B C 

abstract D extends A 

E F G

produces an incorrect model

abstract 0 .. * c1_A : clafer 0 .. * {  }
0 .. * c2_B : clafer 1 .. 1 {  }
0 .. * c3_C : clafer 1 .. 1 {  }
abstract 0 .. * c4_D : clafer 0 .. * {  }
0 .. * c5_extends : clafer 1 .. 1 {  }
0 .. * c6_A : clafer 1 .. 1 {  }
0 .. * c7_E : clafer 1 .. 1 {  }
0 .. * c8_F : clafer 1 .. 1 {  }
0 .. * c9_G : clafer 1 .. 1 {  }

but the compiler should produce a syntax error.

In order to fully support example-driven modeling, every instance of a Clafer model must be a valid model itself, which reproduces exactly that single instance. For example, for a model:

a -> integer 2
   b -> a ?

A possible instance is

a$1 : a -> 5
    b$1 : b -> a$2
a$2 : a -> 6

Note, the instance generators would have to begin using -> 5 instead of = 5, as currently for values.

To allow the instance to always be a valid model (in a sense that when I copy paste the instance into a model, it should just compile and IG should always reproduce the same instance), clafers must be allowed to inherit from concrete clafers: a$1 : a, a$2 : a, and b$1 : b.

So this should be a valid model:

a -> integer 2
   b -> a ?

a$1 : a -> 5
    b$1 : b -> a$2
a$2 : a -> 6

for which the instance generator should produce exactly this instance:

a$1 : a -> 5
    b$1 : b -> a$2
a$2 : a -> 6

Implementation

There are a few considerations

1. allow $<num> in clafer names
2. disallow group cardinality refinement
3. allow adding new children as usual
4. instance generator should not add additional numerals to names, so that we don't end up with a$1$1 and a$2$1. The names which include the $<num> will be required to be unique and checked, therefore IG will not have to add new suffixes.

So, the users should be able to then take a generated instance an edit. There are two reasons:

1. just add more detail, like new children
2. remove detail to create a partial instance

For example, consider this changed model

a$1 : a                      // removed concrete value
    b$1 : b -> a$2
        c                        // added a child
a$2 : a -> 6
     d

Often in models with deeply nested structures, referring to a nested clafer requires long navigation paths, which contain costly . operations. However, when the referred clafer has global cardinality <= 1, then he path can be omitted and the clafer can be referred to globally.

For example

a
   xor b ?
      c 
      d
           e
[ a.b.d.e ]

can be optimized to

[ e ]

that is, e can be accessed the same way as a top-level clafer (e.g., a).

Using compiler v. 0.0.3

abstract Book
author -> Author 1..*

A : Author
B : Author

SomeBook : Book
[ author = A + B ]

Error message

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 24 | Abstract: 2 | Concrete: 20 | References: 2
Constraints: 3
Global scope: 1..*
All names unique: False

[Saving File]
clafer3: IPlus type error

Clafer v0.2.27-1-2012

XML validation does not pass for the model

abstract A
    a : integer


A1 : A
    [ a = 10 ]

Output:

Parse Successful!
[Desugaring]
[Resolving]
[Analyzing String]
[Optimizing]
[Generating Code]
All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0
Constraints: 1
Global scope: 1..*
All names unique: False

[Saving File]
Validation error on line 1, column 2525
cvc-elt.4.3: Type 'cl:IInteger' is not validly derived from the type definition, 'IType', of element 'Type'.

Having installed cabal-install-1.22 and ghc-7.10.3, I set up a Cabal sandbox and followed the instructions for installing with cabal-install, namely:

cabal update
cabal install alex happy
cabal install clafer

Installation failed with the message:

src/Language/Clafer/Front/LexClafer.x:188:38:
    Not in scope: ‘ord’
    Perhaps you meant one of these:
      ‘or’ (imported from Prelude), ‘odd’ (imported from Prelude),
      ‘ord#’ (imported from GHC.Exts)
Failed to install clafer-0.4.3

Should this file explicitly import Data.Char (ord)?

I have done a bit of testing on if-then-else with clafer compiler. I tried both 0.3.6.1 and 0.4.0. They do differ a bit in handling my examples, but both seem to require that the subexpressions are (almost?) always parenthesized as in if (...) then (some ...) else (a.b.c) .

This is quite non-standard in programming languages. Usually the ternary operator gets a very low precedence and if - then -else can be written without parenthesis. I think this is both in C like languages (? :) and in ML-like languages (if-then-else).

This is not super urgent but we could consider looking into the grammar to fix it. Usability for users would improve slightly.

Hi,

I tried to access the binary distribution via the link on the wiki (and clafer.org) and I'm getting 404 Not Found.

Are the binaries still available?

Thanks.

The "dref problem" is a situation whereby the compiler cannot figure out whether a reference clafer should be automatically dereferenced or not. In such situations, the model is usually inconsistent and hard to debug.

A compiler could issue a warning that a reference clafer was not dereferenced. In some cases, it is intentional but in most cases it leads to an inconsistent model.

warning: a reference clafer `a` in expression `this.a = parent.b.a` not dereferenced automatically which may cause the model to be inconsistent. Add the ".dref" if needed.

Also, another way of dealing with that problem is to look at the desugared clafer output.