Faculty of Engineering and Mathematical Sciences 
Not logged in (login)

help5501

This forum is provided to promote discussion amongst students enrolled in CITS5501 Software Testing and Quality Assurance.

Before posting a question here, you might like to (1) search the forum for previous posts asking the same question, and (2) read the article How To Ask Questions The Smart Way .
And please keep the discussion civil (as required by UWA's Computer Use Policy, #9).
 

Options:
RSS cloud
Jump to:

Workshop question - Omnivore

1 of 124 articles shown, currently no other people reading this forum.
photo
From: Arran S.
Date: Wed 20th May 2020, 5:13pm
Actions: 
        Login-to-reply

 

That looks correct - I managed to temporarily forget during the workshop that you can use 
"in" in a sig.

If you want to check that this works the way you want, a typical way to do this is:

- assert something we *think* should always be true
- ask alloy if it can find a counter-example, using the "check" command.

Some things we could try checking: if our model works as expected, then it shouldn't be 
possible to have an omnivore which is not a herbivore, or an omnivore which is not a 
carnivore.

assert allOmnisAreHerb {
   #(omnivore - herbivore) = 0
}

check allOmnisAreHerb for 3

assert allOmnisAreCarn {
   #(omnivore - carnivore) = 0
}

check allOmnisAreCarn for 3

(There are a few different ways of expressing it, but the above I hope is self-explanatory.)

If we run this, Alloy should say something like:


Executing "Check noNoHerbs for 4"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   121 vars. 16 primary vars. 205 clauses. 5ms.
   No counterexample found. Assertion may be valid. 2ms.

.

Executing "Check allOmnisAreHerb for 4"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   121 vars. 16 primary vars. 205 clauses. 3ms.
   No counterexample found. Assertion may be valid. 1ms.

.. meaning it can't find any "possible world" which is a counterexample to our assertion.

If our system were more complicated, we might try increasing 3 to larger and larger numbers, 
to increase the number of possibilities that are checked.

cheers

Arran 


ANONYMOUS wrote:

> i think this works as alloy code for omnivore btw for anyone in the workshop wondering
> 
> Can anyone else confirm?
> 
> sig animal {}
> 
> sig herbivore in animal {}
> sig carnivore in animal {}
> 
> sig omnivore in animal {}
> 
> fact omni {
> omnivore in herbivore and omnivore in carnivore
> }
> 
> fact {
> 
> 	herbivore & carnivore = omnivore
> 
> }

Related articles

Workshop question - Omnivore (all 5) RSS
├─ original   Wed 20th May 2020, 4:57pm, ANONYMOUS
├─ reply 1   Wed 20th May 2020, 4:59pm, ANONYMOUS  O.P.
├─ THIS   Wed 20th May 2020, 5:13pm, Arran S.
├─ reply 3   Thu 4th Jun 2020, 4:12pm, ANONYMOUS
└─ reply 4   Fri 5th Jun 2020, 3:30pm, Arran S.
This Page


Program written by: [email protected]
Feedback welcome
Last modified: 11:27am Sep 21 2020