gsdlab/clafer — Issue #10: Incorrect translation of integers to Alloy
Author: mantkiew
Created: 2011-12-18 02:33:54+00:00
State: open

Version: 0.0.3

For a model:

```clafer
A
x : integer
[ x >= 0 ]
```

the resulting Alloy model is correct:

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

However, for a Clafer model

```clafer
A
x : integer
[ this >= 0 ]
```

the resulting Alloy model is incorrect:

```alloy
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 constrain should be

```alloy
...
{ 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.