instance type

[w.icelander]

//------------------------------------------------
module output
abstract sig Class1 {}   //define signature class1
abstract sig Class2 {}   //define signature class2

one sig instance1 extends Class1 {}  //define a single instance
one sig instance2 extends Class2 {}  //define a single instance

pred example(){}

pred testtype(){   //i want to test what type instance1 belongs to?
 some instance1
 instance1 = Class1
}
run example
run testtype
//-------------------------------------------------

This module above creates two instances called instance1, instance2
they happen to be of two different types namely Class1,Class2
respectively.

Question-1: Assuming I have no access to the code, how can I find the
type of an instance or test it?

Question-2:  I tried experimenting with the code, and i wrote the test
type predicate. The predicate testtype complies as long as instance1
is equated with Class1.  Does this code produce the correct result?

Question-3: I visualized the model, in the evaluator i executed
 
instance1=Class2

it came back with FALSE  which is what I expected.  Again is this a
valid test?

[Felix Chang-2]

On Sun, 20 Apr 2008, w.icelander wrote:

> abstract sig Class1 {}
> abstract sig Class2 {}
> one sig instance1 extends Class1 {}
> one sig instance2 extends Class2 {}
>
> pred testtype { // i want to test what type instance1 belongs to?
> some instance1
> instance1 = Class1
> }
>
> Question-1: Assuming I have no access to the code,
> how can I find the type of an instance or test it?

I don't think I understand the question.
When you say you don't have access to the code, do you mean
when you don't have access to part of the Alloy model?
But if you don't have access to a piece of Alloy model that you need,
then you would not be able to import it and check against it either.
So... I'm afraid I would need a more concrete example for that.

> Question-2:  I tried experimenting with the code, and i wrote the test
> type predicate. The predicate testtype complies as long as instance1
> is equated with Class1.  Does this code produce the correct result?

"some instance1" is always true, since you declared "one sig instance1"
and so instance1 always contains exactly one atom; no more, and no less.

"instance1 = Class1" is only true when class1 has only one atom.
In general, I suspect you want to say "instance1 in Class1" instead.

> Question-3: I visualized the model, in the evaluator i executed
> instance1=Class2
> it came back with FALSE  which is what I expected.
> Again is this a valid test?

"instance1=Class2" is indeed false.  But I suspect what you really
want to test is "instance1 !in Class2".

Sincerely,
Felix Chang
Alloy4 Developer

[w.icelander]

Thanks Felix,  
this is what I was looking for : instance1 in Class1
Regards


--- In alloy-discuss@..., Felix Chang <fschang@...> wrote:

>
> On Sun, 20 Apr 2008, w.icelander wrote:
> > abstract sig Class1 {}
> > abstract sig Class2 {}
> > one sig instance1 extends Class1 {}
> > one sig instance2 extends Class2 {}
> >
> > pred testtype { // i want to test what type instance1 belongs to?
> > some instance1
> > instance1 = Class1
> > }
> >
> > Question-1: Assuming I have no access to the code,
> > how can I find the type of an instance or test it?
>
> I don't think I understand the question.
> When you say you don't have access to the code, do you mean
> when you don't have access to part of the Alloy model?
> But if you don't have access to a piece of Alloy model that you need,
> then you would not be able to import it and check against it either.
> So... I'm afraid I would need a more concrete example for that.
>
> > Question-2:  I tried experimenting with the code, and i wrote the test
> > type predicate. The predicate testtype complies as long as instance1
> > is equated with Class1.  Does this code produce the correct result?
>
> "some instance1" is always true, since you declared "one sig instance1"
> and so instance1 always contains exactly one atom; no more, and no less.
>
> "instance1 = Class1" is only true when class1 has only one atom.
> In general, I suspect you want to say "instance1 in Class1" instead.
>
> > Question-3: I visualized the model, in the evaluator i executed
> > instance1=Class2
> > it came back with FALSE  which is what I expected.
> > Again is this a valid test?
>
> "instance1=Class2" is indeed false.  But I suspect what you really
> want to test is "instance1 !in Class2".
>
> Sincerely,
> Felix Chang
> Alloy4 Developer
>