Test cases for Alloy

Experimental
1

I am looking for test cases for Alloy. Test cases can be written in Alloy. For example, the following is a test of some integer operations. During the build, we run all these tests and verify their expected outcomes. (expect 0 is no solution).

It would be nice to have test cases for all of Alloy’'s operations to make sure that any changes in the code won’t affect the results.

--option                noOverflow=false
--option.noOvflw_*      noOverflow=true

sig NonInt {}

equal:             run { 1=1                      } expect 1
equal2:            run { all n : Int | n = n      } expect 1
equal3:            run { some n : Int | n = 1     } expect 1

unequal:           run { 1!=1                       } expect 0
plus:              run { 1.plus[1]=2                } for 4 int expect 1
xplus:             run { 1.plus[1]!=2               } for 4 int expect 0
minus:             run { 1.minus[1]=0               } for 4 int expect 1
xminus:            run { 1.minus[1]!=0              } for 4 int expect 0
div:               run { 4.div[2]=2                 } for 4 int expect 1
xdiv:              run { 4.div[2]!=2                } for 4 int expect 0
div_min:           run { 4.div[-2]=-2               } for 4 int expect 1
xdiv_min:          run { 4.div[-2]!=-2              } for 4 int expect 0
mul:               run { 4.mul[2]=8                 } for 5 int expect 1
xmul:              run { 4.mul[2]!=8                } for 5 int expect 0
mul_min:           run { 4.mul[-2]=-8               } for 5 int expect 1
xmul_min:          run { 4.mul[-2]!=-8              } for 5 int expect 0

max_4:             run { 7 in Int and -8 in Int     } for 4 int expect 1

 // TODO this fails but I think it should fail to compile
 // noOvflw_max_4_9:  run { 9 in Int                 } for 4 int expect 0
 // xmax_4:         run { 9 not in Int               } for 4 int expect 1

max_5:             run { 15 in Int and -16 in Int   } for 5 int expect 1
max_6:             run { 31 in Int and -32 in Int   } for 6 int expect 1
max_7:             run { 63 in Int and -64 in Int   } for 7 int expect 1
max_8:             run { 127 in Int and -128 in Int } for 8 int expect 1
max_9:             run { 255 in Int and -256 in Int } for 9 int expect 1

intinuniv:         run { all n : Int | n in univ    } for 4 int expect 1
intinident:        run { all n : Int | n->n in iden } for 4 int expect 1
inset:             run { 1 in  { n : Int | n = n }  } for 4 int expect 1
inset2:            run { 1 in  (-1+0+1+2)           } for 4 int expect 1
noother:           run { no n : Int | n in NonInt   } for 4 int expect 1

noOvflw_plus:      run { 6.plus[6]=-4               } for 4 int expect 0
okOverflow:        run { 6.plus[6]=-4               } for 4 int expect 1

pred solvesum[x,y,z : Int ] {
    x.plus[y] = z
}
solvesum_0:          run { some x,y,z : Int | solvesum[x,y,z]     } for 4 int expect 1
solvesum_1:          run { some x,y,z : Int | solvesum[x,y,z] and x > y and y > z    } for 4 int expect 1

So don’t ask what Alloy can do for you, ask what you can do for Alloy! :slight_smile: Nice task when you got a few minutes.

You can just post them here in this topic. I promise to give them a like!

2

Is that what you’re thinking about?

abstract sig Object {}

sig File extends Object {}

sig Dir extends Object {
	entries: set Entry
}

one sig Root extends Dir {}

sig Name {}

sig Entry {
	name: one Name,
	object: one Object
}

one sig Entry0, Entry1, Entry2, Entry3 extends Entry {}
one sig Name0, Name1, Name2, Name3 extends Name {}
one sig Dir0, Dir1 extends Dir {}
one sig File0 extends File {}

fact {
	#Entry = 4
	#Name = 4
	#Object = 4
	name = Entry1 -> Name2 + Entry0 -> Name0 +
         Entry2 -> Name1 + Entry3 -> Name1
	entries = Root -> Entry1 + Root -> Entry0 + Root -> Entry2 +
            Dir0 -> Entry3
	object = Entry1 -> File0 + Entry0 -> File0 +
           Entry2 -> Dir0 + Entry3 -> Dir1
}


check Union {
	File + Dir = Root + Dir0 + Dir1 + File0
} expect 0

check Intersection {
	Dir1 & Dir = Dir1
	Root & Dir = Root
} expect 0

check Difference {
	Dir - Object =  none
} expect 0

check Dot01 {
	Root.entries = Entry0 + Entry1 + Entry2
} expect 0

check Dot02 {
	Root.entries.name = Name0 + Name1 + Name2
} expect 0

I can define more test cases for relational operators, if that’s the kind of spec you think can help for regression tests.

1 Like
3

Thanks for engaging, appreciated.

Personally, but I am open for disagreement, I’d like the test cases to be more direct. You use Object,File,Dir, and Root but you actually don’t have their semantics. I feel your pain, for test cases you need atoms …

Although integers are not recommended in Alloy, they do have the huge advantage that you got lots of atoms that you directly use in your code. I think (but maybe someone else can weigh in) that although Int’s have some special semantics, for set operations they are really treated as atoms. So personally I think we should take advantage of this.

So my attempt to test the relational operators would look like:

let s1  = (1+2+3)
let s2  = (4+5+6)
let s3  = (3+4)
let neg = { n : Int | n < 0 }
let pos = { n : Int | n > 0 }
let s4  = (s1 -> s2)

run union               { s1 + s2 = (1+2+3+4+5+6)   } expect 1
run intersection_no     { s1 & s2 = none            } expect 1
run intersection_one    { s1 & s3 = 3               } expect 1
run intersection_one    { s1 & s3 = 3               } expect 1
run intersection_parent { Int & s1 = s1             } expect 1
run differencee         { s1 - s3 = 1+2             } expect 1
run complete            { Int - neg = 0 + pos       } for 4 int expect 1
run block_join          { s4[s1] = s2               } expect 1
run dot_join            { s1.s4  = s2               } expect 1

Now you are using check with expect 0. Is there a logical difference?

4

Yes, to specify test cases, I need atoms. So I just defined some. The configuration is a concrete instance of a file system as used in https://haslab.github.io/formal-software-design/structural-design/index.html.

I agree that your approach is more concise. But seeing the test cases as typical examples, I think my approach can be used as a kind of tutorial too.

I used check because that’s the usual way in Alloy to see if an assertion is true.

5

The thing that I felt was odd was that the model did not have behavior defined for File, Root, Dir, etc. So the names implied something that wasn’t there, which confused me initially. I also had to look very carefully at your testcases to see if the expected outcome was correct.

That said, it is always a problem to get your hand on atoms in Alloy since you immediately get a lot of semantics involved. One way is to use a predicate:

  sig Atom {}
  pred union( disj a, b, c, d, e, f, g, h, i, j : Atom ) { a+b = b+a }
  run union for 10 Atom expect 1

But that extra code seems rather ungrateful to the 16 integers we always get for free :slight_smile:

Yeah, I am not sure really why run feels better in this case … A check tests if there is a counter example, I am struggling a bit to see how it maps to a test case? Finding or not funding a counter example depends on the test case? Since they are logically equivalent I think the ‘positive’ run is easier to understand, but I am open to be convinced otherwise?

I hope I am not putting you off … I am struggling how to do this in this world between Java & Alloy. Since there are very few test cases today, I’d like to get start the best we can. But I do not claim any expertise how to best do this.

6

Hi Peter,
here are some tests which we have used when developing Electrum/Alloy 6. Most of these identities come from the SPOT tool documentation.

// modules raises warnings

----------------------------------------------------------------------
var sig V {}

t6: run { eventually V != V' } expect 1

t8: run { always V = V' } expect 1

t10: run { always eventually V = V' and always eventually V != V' } expect 1

----------------------------------------------------------------------
var lone sig W {}

t15: check { always lone W } expect 0

t17: run { eventually (some x: W | eventually some y: W | x != y) } expect 1

t19: run { some x: W | always W in x } expect 1

----------------------------------------------------------------------
var some sig Y {}

t24: check { always some Y } expect 0

t26: run { some x: Z | always Z in x } expect 1

----------------------------------------------------------------------
var one sig Z {}

t31: check { always lone Z } expect 0

t33: check { always some Z } expect 0

t35: check { always one Z } expect 0

t37: run { eventually (some x: Z | eventually some y: Z | x != y) } expect 1

t39: run { some x: Z | always Z in x } expect 1

----------------------------------------------------------------------
var sig A {}

var sig B, C extends A {}

t46: check { always B in A } expect 0

t48: check { always C in A } expect 0

t50: check { 
	always all x: B, y: C | always (x not in C and y not in B)
} expect 0

----------------------------------------------------------------------
var abstract sig D {}

var sig E, F extends D {}

t59: check { always D in E + F } expect 0

t61: check { always E in D } expect 0

t63: check { always F in D } expect 0

t65: check { 
	always all x: E, y: F | always (x not in F and y not in E)
} expect 0

----------------------------------------------------------------------

var sig G, H, I, J {}

pred p { some G }
pred q { some H }
pred r { some I }
pred s { some J }

pred tt { G = G }
pred ff { G != G }

t81: check { (always after p) iff (after always p) } expect 0

t83: check { always p iff not (eventually not p) } expect 0

t85: check { after ff iff ff } expect 0

t87: check { eventually ff iff ff } expect 0 

t89: check { (after p until q and r) iff (((after p) until q) and r) } expect 0

t91: check { (after tt) iff tt } expect 0
t92: check { (always ff) iff ff } expect 0

t94: check { (eventually tt) iff tt } expect 0
t95: check { (eventually eventually ff) iff eventually ff } expect 0

t97: check { (always tt) iff tt } expect 0
t98: check { (always always ff) iff always ff } expect 0

t100: check { (p until tt) iff tt } expect 0
t101: check { (ff until p) iff p } expect 0
t102: check { (p until ff) iff ff } expect 0
t103: check { (p until p) iff p } expect 0
t104: check { (tt until p) iff eventually p } expect 0
t105: check { ((after p) until (after q)) iff after (p until q) } expect 0

t107: check { (p releases q) iff not ((not p) until (not q)) } expect 0
t108: check { (p releases tt) iff tt } expect 0
t109: check { (p releases ff) iff ff } expect 0
t110: check { (tt releases p) iff p } expect 0
t111: check { (p releases p) iff p } expect 0
t112: check { (ff releases p) iff always p } expect 0
t113: check { (p releases q) iff (q and (p or after (p releases q))) } expect 0

t115: check { (after eventually always p) iff eventually always p } expect 0
t116: check { (after always eventually p) iff always eventually p } expect 0
t117: check { (after eventually p) iff eventually after p } expect 0

t119: check { (eventually (p until q)) iff eventually q } expect 0
t120: check { (eventually always (p and after q)) iff eventually always (p and q) } expect 0 
t121: check { (eventually always (p and always q)) iff eventually always (p and q) } expect 0
t122: check { (eventually always (p or always q)) iff eventually (always p or always q) } expect 0
t123: check { (eventually always (p and eventually q)) iff ((eventually always p) and always eventually q) } expect 0
t124: check { (eventually always (p or eventually q)) iff ((eventually always p) or always eventually q) } expect 0

t126: check { (always eventually (p or after q)) iff always eventually (p or q) } expect 0
t127: check { (always eventually (p or eventually q)) iff always eventually (p or q) } expect 0
t128: check { (always eventually (p and eventually q)) iff always (eventually p and eventually q) } expect 0
t129: check { (always eventually (p and always q)) iff ((always eventually p) and eventually always q) } expect 0
t130: check { (always eventually (p or always q)) iff ((always eventually p) or eventually always q) } expect 0

t132: check { (p until always p) iff always p } expect 0
t133: check { (p releases (eventually p)) iff eventually p } expect 0


t136: check { (eventually always p and eventually always q) iff eventually always (p and q) } expect 0
t137: check { (after p and after q) iff after (p and q) } expect 0
t138: check { (after p and eventually always q) iff after (p and eventually always q) } expect 0
t139: check { ((p until q) and (r until q)) iff ((p and r) until q) } expect 0
t140: check { ((p releases q) and (p releases r)) iff (p releases (q and r)) } expect 0
t141: check { ((p until q) or (p until r)) iff (p until (q or r)) } expect 0
t142: check { ((p releases q) or (r releases q)) iff ((p or r) releases q) } expect 0

t144: check { ((always q) or (p releases q)) iff (p releases q) } expect 0


t147: check { ((after p) releases (after q)) iff after (p releases q) } expect 0

t149: check { (always (p releases q)) iff always q } expect 0 

t151: check { eventually always once p iff eventually p } expect 0

t153: check { eventually (p and (q since r)) iff eventually (r and (p or after (q until (q and p)))) } expect 0
7

Thanks! Included in the test directory, they are now always tested.

8

Notice many tests at the beginning of the file aren’t useful, I think you can get rid of them.

9

Well, they have zero cost and who know, they might test something useful one day :slight_smile: But once they are committed, feel free to expand/update them.

The checks look cool. Have to do some thinking why you use some instead of one in the pred's?

10

I guess I just needed any preds and I wrote this in a hurry (BTW the definition of tt and ff could be simplified too).

11

I think it is an interesting issue. I don’t think there is a recommended way to have some instances you can play with in a test?

I see the predicate route:

 pred foo( disj a, b, c, d, e : Foo ) { ... }
 run foo

Or the sig route:

sig Object {}
sig a,b,c,d,e extends Object {}

Or the ‘some’ route:

run { 
      some disj a,b,c,d,e : Foo { ... }
}
12

We’ve done some work with “unit” test cases for Alloy that we have then used for mutation testing/fault localization/repair. It follows the predicate route you motioned and it is designed to outline a specific instance and then you would use a command to say if the instance should be allowed or prevented by some formulas in the model.

For example, for a singly linked list model with a List, Node, header, and link, we’d outline the following:

pred three_node_list {
   some l0 : List | some disj n0, n1, n2 : Node {
      List = l0
      Node = n0 + n1 + n2
      header = l0->n0
      link = n0->n1 + n1->n2
   }   
}
1 Like