Odd behaviour, possible bug

[jasonreich_uk]

Hey everybody,

I've got some odd code.

abstract sig A {}
abstract sig B1 extends A {}
abstract sig B2 extends A {}
one sig C extends B1 {}

check {
        A = C
} for 8

I'd expect this assertion to be correct but Alloy 4.1.2 says that a counterexample exists
where B2 suddenly comes in non-abstract existence.

Am I expectations correct or is Alloy's behaviour correct?

Thanks in advance,
Jason

[Felix Chang-2]

On Fri, 18 Apr 2008, Jason Reich wrote:

> abstract sig A {}
> abstract sig B1 extends A {}
> abstract sig B2 extends A {}
> one sig C extends B1 {}
> check { A = C } for 8
>
> I'd expect this assertion to be correct but Alloy 4.1.2 says
> that a counterexample exists
> where B2 suddenly comes in non-abstract existence.
>
> Am I expectations correct or is Alloy's behaviour correct?

Dear Jason:

This is not a bug.

The "abstract" keyword is ignored if a sig has no subsig.
This has been the behavior for both Alloy3 and Alloy4.

For Alloy3 users, please see page 21 of Alloy 3 reference manual
http://alloy.mit.edu/reference-manual.pdf or page 268 of
Daniel Jackson's "Software Abstractions" book for more explaination.

For Alloy4 users, this is explained in Chapter 1, File System Lesson 1
in Alloy4's online tutorial http://alloy.mit.edu/alloy4/tutorial4/

Thank you again for trying the Alloy Analyzer, and please let me know
if you have any further questions.

Sincerely,
Felix Chang
Alloy4 Developer