how to express condition

[ylayouni]

Hello Alloy users

please how can we build a condition like this :

for all user.Zone=sectionA then those user.state=low

i try to do this :
fact {
user.Zone=sectionA => user.state=low
}

but the analyzer dont applies this condiction for all users !!

thank you

[Irina Rychkova]

Try this:
{all user: User | user.Zone = sectionA => user.state =low
}

From: alloy-discuss@... [mailto:alloy-discuss@...] On Behalf Of ylayouni
Sent: 24 June 2008 23:40
To: alloy-discuss@...
Subject: [alloy-discuss] how to express condition


Hello Alloy users

please how can we build a condition like this :

for all user.Zone=sectionA then those user.state=low

i try to do this :
fact {
user.Zone=sectionA => user.state=low
}

but the analyzer dont applies this condiction for all users !!

thank you

[Felix Chang-2]

On Tue, 24 Jun 2008, ylayouni wrote:
> for all user.Zone=sectionA then those user.state=low
>
> i try to do this :
> fact {
> user.Zone=sectionA => user.state=low
> }

I assume "user" is a signature, perhaps looking like this:

sig user {
   Zone: ...
}

In that case, you need to write your fact like this:

fact {
   all u: user | u.Zone=sectionA => u.state=low
}

What you wrote doesn't work, because what you wrote only applies
when EVERY user have zone=sectionA.  That is, if there is at least
one user whose zone is not sectionA, then your rule doesn't apply!

Sincerely,
Felix Chang
Alloy4 Developer

[Jeremy Jacob]

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

>
> On Tue, 24 Jun 2008, ylayouni wrote:
> > for all user.Zone=sectionA then those user.state=low
> >
> > i try to do this :
> > fact {
> > user.Zone=sectionA => user.state=low
> > }
>
> I assume "user" is a signature, perhaps looking like this:
>
> sig user {
>    Zone: ...
> }
>
> In that case, you need to write your fact like this:
>
> fact {
>    all u: user | u.Zone=sectionA => u.state=low
> }

If you don't like quantifiers you could also write:

fact{Zone.sectionA in state.low}

although some people would argue that this is too opaque (a change in
the names ou use might fix that).

[pierrekelsen]

--- In alloy-discuss@..., "Jeremy Jacob"
<Jeremy.Jacob@...> wrote:

>
> --- In alloy-discuss@..., Felix Chang <fschang@> wrote:
> >
> > On Tue, 24 Jun 2008, ylayouni wrote:
> > > for all user.Zone=sectionA then those user.state=low
> > >
> > > i try to do this :
> > > fact {
> > > user.Zone=sectionA => user.state=low
> > > }
> >
> > I assume "user" is a signature, perhaps looking like this:
> >
> > sig user {
> >    Zone: ...
> > }
> >
> > In that case, you need to write your fact like this:
> >
> > fact {
> >    all u: user | u.Zone=sectionA => u.state=low
> > }
>
> If you don't like quantifiers you could also write:
>
> fact{Zone.sectionA in state.low}
>
> although some people would argue that this is too opaque (a change in
> the names ou use might fix that).
>

Or use a signature fact:
sig user {...
}{ Zone = sectionA => state=low}
(also avoids use of quantifiers).

[ylayouni]

--- In alloy-discuss@..., "pierrekelsen"
<pierre.kelsen@...> wrote:
>
> --- In alloy-discuss@..., "Jeremy Jacob"
> <Jeremy.Jacob@> wrote:
> >
> > --- In alloy-discuss@..., Felix Chang <fschang@>
wrote:

> > >
> > > On Tue, 24 Jun 2008, ylayouni wrote:
> > > > for all user.Zone=sectionA then those user.state=low
> > > >
> > > > i try to do this :
> > > > fact {
> > > > user.Zone=sectionA => user.state=low
> > > > }
> > >
> > > I assume "user" is a signature, perhaps looking like this:
> > >
> > > sig user {
> > >    Zone: ...
> > > }
> > >
> > > In that case, you need to write your fact like this:
> > >
> > > fact {
> > >    all u: user | u.Zone=sectionA => u.state=low
> > > }
> >
> > If you don't like quantifiers you could also write:
> >
> > fact{Zone.sectionA in state.low}
> >
> > although some people would argue that this is too opaque (a

change in
> > the names ou use might fix that).
> >
>
> Or use a signature fact:
> sig user {...
> }{ Zone = sectionA => state=low}
> (also avoids use of quantifiers).

thank you very much

all u: user | u.Zone=sectionA => u.state= u.state + low

this is to preserve the old state

thank you