Checking Multiple Assertions

[w.icelander]

I have the following module, ignore the semantics, the question is at
the end.
//===============
module test

abstract sig role{}{}

one sig person extends role{
     acts: some role
      }
assert Provision1{
 some person.~acts
}

assert Provision2{
 some person
}

check Provision1
check Provision2
//======================================
This module compiles as is.  What I want to do is have an agregate
assertion.
ie. check Provision1 & Provision2
I know it doesnt compile, is there a way of doing so.
thanks
Will

[Felix Chang-2]

On Sat, 19 Apr 2008, w.icelander wrote:

> assert Provision1 { some person.~acts }
> assert Provision2 { some person }
> check Provision1
> check Provision2
>
> This module compiles as is.  What I want to do is have
> an agregate assertion. ie. check Provision1 & Provision2
> I know it doesnt compile, is there a way of doing so.
> thanks
> Will

Dear Will:

I have two suggestions for doing this.

(1) Keep your model as is.  Then you simply go to the Execute
menu at the top of Alloy4 GUI, and you can click "Execute All"
which will perform every check you wrote in the model, and
will provide a grand summary of successes and failures afterwards.

2) Alternatively, you can change your "assert" into "pred", and then
you can check them one at a time or combine them (using the { } syntax):
pred Provision1 { some person.~acts }
pred Provision2 { some person }
check { Provision1 }
check { Provision2 }
check { Provision1 && Provision2 }

Sincerely,
Felix Chang
Alloy4 Developer

[Felix Chang-2]

On Fri, 18 Apr 2008, Felix Chang wrote:
> 2) Alternatively, you can change your "assert" into "pred", and then
> you can check them one at a time or combine them (using the { } syntax):
> pred Provision1 { some person.~acts }
> pred Provision2 { some person }
> check { Provision1 }
> check { Provision2 }
> check { Provision1 && Provision2 }

One more note: If you write it like what I showed above, then these 3 checks
will be called "check$1" "check$2" and "check$3" which is not very intuitive.

Fortunately, you can prepend "name:" in front of each CHECK command, like this:

Acyclic: check { Provision1 }
Balanced: check { Provision2 }
Acyclic_and_balanced: check { Provision1 && Provision2 }

Then in the Alloy Analyzer's Execute Menu, and in the Analyzer Output,
these 3 commands will show up as "Acyclic", "Balanced",
and "Acyclic_and_Balanced" (rather than "Check$1" "Check$2" "Check$3")

Sincerely,
Felix Chang
Alloy4 Developer

[Daniel Le Berre]

Dear Will,

In Alloy 4 Eclipse, you can easily  select  multiple check or run
commands, as illustrated in the enclosed screenshot.

You can get A4E from http://alloy4eclipse.googlecode.com/

    Daniel

Felix Chang a écrit :

> On Sat, 19 Apr 2008, w.icelander wrote:
>  
>> assert Provision1 { some person.~acts }
>> assert Provision2 { some person }
>> check Provision1
>> check Provision2
>>
>> This module compiles as is.  What I want to do is have
>> an agregate assertion. ie. check Provision1 & Provision2
>> I know it doesnt compile, is there a way of doing so.
>> thanks
>> Will
>>    
>
> Dear Will:
>
> I have two suggestions for doing this.
>
> (1) Keep your model as is.  Then you simply go to the Execute
> menu at the top of Alloy4 GUI, and you can click "Execute All"
> which will perform every check you wrote in the model, and
> will provide a grand summary of successes and failures afterwards.
>
> 2) Alternatively, you can change your "assert" into "pred", and then
> you can check them one at a time or combine them (using the { } syntax):
> pred Provision1 { some person.~acts }
> pred Provision2 { some person }
> check { Provision1 }
> check { Provision2 }
> check { Provision1 && Provision2 }
>
> Sincerely,
> Felix Chang
> Alloy4 Developer
>
>
>
> ------------------------------------
>
> Yahoo! Groups Links
>
>
>
>
>
>  

--
           Daniel Le Berre mailto:leberre@...
           MCF,    CRIL-CNRS UMR 8188,    Universite d'Artois
           http://www.cril.univ-artois.fr/~leberre


 

[w.icelander]

Daniel,

Does that mean that all assertions are evaluated at the same time.

.will

--- In alloy-discuss@..., Daniel Le Berre <leberre@...> wrote:

>
> Dear Will,
>
> In Alloy 4 Eclipse, you can easily  select  multiple check or run
> commands, as illustrated in the enclosed screenshot.
>
> You can get A4E from http://alloy4eclipse.googlecode.com/
>
>     Daniel
>
> Felix Chang a écrit :
> > On Sat, 19 Apr 2008, w.icelander wrote:
> >  
> >> assert Provision1 { some person.~acts }
> >> assert Provision2 { some person }
> >> check Provision1
> >> check Provision2
> >>
> >> This module compiles as is.  What I want to do is have
> >> an agregate assertion. ie. check Provision1 & Provision2
> >> I know it doesnt compile, is there a way of doing so.
> >> thanks
> >> Will
> >>    
> >
> > Dear Will:
> >
> > I have two suggestions for doing this.
> >
> > (1) Keep your model as is.  Then you simply go to the Execute
> > menu at the top of Alloy4 GUI, and you can click "Execute All"
> > which will perform every check you wrote in the model, and
> > will provide a grand summary of successes and failures afterwards.
> >
> > 2) Alternatively, you can change your "assert" into "pred", and then
> > you can check them one at a time or combine them (using the { }

syntax):

> > pred Provision1 { some person.~acts }
> > pred Provision2 { some person }
> > check { Provision1 }
> > check { Provision2 }
> > check { Provision1 && Provision2 }
> >
> > Sincerely,
> > Felix Chang
> > Alloy4 Developer
> >
> >
> >
> > ------------------------------------
> >
> > Yahoo! Groups Links
> >
> >
> >
> >
> >
> >  
>
>
> --
>            Daniel Le Berre mailto:leberre@...
>            MCF,    CRIL-CNRS UMR 8188,    Universite d'Artois
>            http://www.cril.univ-artois.fr/~leberre
>

[Daniel Le Berre]

Will,

It means that all selected commands will be evaluated (one after the other).

You can configure the plugin to show you automatically models or counter
examples found.

If you want to rerun exactly the same set of commands, then you just
need to hit Ctrl-F11, which is the usual way to rerun a command inside
Eclipse.

Cheers,

    Daniel

w.icelander a écrit :

> Daniel,
>
> Does that mean that all assertions are evaluated at the same time.
>
> .will
>
> --- In alloy-discuss@..., Daniel Le Berre <leberre@...> wrote:
>  
>> Dear Will,
>>
>> In Alloy 4 Eclipse, you can easily  select  multiple check or run
>> commands, as illustrated in the enclosed screenshot.
>>
>> You can get A4E from http://alloy4eclipse.googlecode.com/
>>
>>     Daniel
>>
>> Felix Chang a écrit :
>>    
>>> On Sat, 19 Apr 2008, w.icelander wrote:
>>>  
>>>      
>>>> assert Provision1 { some person.~acts }
>>>> assert Provision2 { some person }
>>>> check Provision1
>>>> check Provision2
>>>>
>>>> This module compiles as is.  What I want to do is have
>>>> an agregate assertion. ie. check Provision1 & Provision2
>>>> I know it doesnt compile, is there a way of doing so.
>>>> thanks
>>>> Will
>>>>    
>>>>        
>>> Dear Will:
>>>
>>> I have two suggestions for doing this.
>>>
>>> (1) Keep your model as is.  Then you simply go to the Execute
>>> menu at the top of Alloy4 GUI, and you can click "Execute All"
>>> which will perform every check you wrote in the model, and
>>> will provide a grand summary of successes and failures afterwards.
>>>
>>> 2) Alternatively, you can change your "assert" into "pred", and then
>>> you can check them one at a time or combine them (using the { }
>>>      
> syntax):
>  
>>> pred Provision1 { some person.~acts }
>>> pred Provision2 { some person }
>>> check { Provision1 }
>>> check { Provision2 }
>>> check { Provision1 && Provision2 }
>>>
>>> Sincerely,
>>> Felix Chang
>>> Alloy4 Developer
>>>
>>>
>>>
>>> ------------------------------------
>>>
>>> Yahoo! Groups Links
>>>
>>>
>>>
>>>
>>>
>>>  
>>>      
>> --
>>            Daniel Le Berre mailto:leberre@...
>>            MCF,    CRIL-CNRS UMR 8188,    Universite d'Artois
>>            http://www.cril.univ-artois.fr/~leberre
>>
>>    
>
>
>
> ------------------------------------
>
> Yahoo! Groups Links
>
>
>
>
>
>  

--
           Daniel Le Berre mailto:leberre@...
           MCF,    CRIL-CNRS UMR 8188,    Universite d'Artois
           http://www.cril.univ-artois.fr/~leberre