MM2 Example: Testing Your Code

Just like in other programming languages, you can write tests for your MM2 programs. We demonstrate this using the ancestor example from the Reachability part 1 tutorial. In the ancestor example, we compute all ancestors of selected persons of interest (POIs) based on a family tree.

The program produces statements of the form (ancestor $p $a). We will provide the expected results as (solution $p $a). The test compares produced and expected facts by computing their symmetric difference:

• If a pair appears in both → it is correct.
• If a pair appears in only one → it is a mistake, and we will mark it (MISTAKE $p $a).

Note that in this example, we included wrong solutions for Vic to demonstrate how mistakes are detected.

Another example of MM2 tests can be found in the CTL model checking example

; =============================================
;                 Family tree data
; =============================================
(parent Fred Tom)
(parent Tom Bob) (parent Xey Uru)
(parent Pam Bob) (parent Yip Uru)
(parent Tom Liz) (parent Zac Vic)
(parent Bob Ann) (parent Whu Vic)
(parent Bob Pat) (parent Uru Ohm)
(parent Pat Jim) (parent Vic Ohm)


; =============================================
;                 Ancestor program
; =============================================
(exec (0 0) (, (parent $p $c))
            (, (child $c $p)))

(exec (0 1) (, (poi $c) (child $c $p))
            (, (generation Z $c $p)))

(exec (1 Z) (, (exec (1 $l) $ps $ts)
               (generation $l $c $p) (child $p $gp) )
            (, (exec (1 (S $l)) $ps $ts)
               (generation (S $l) $c $gp) ))

(exec (2 0) (, (generation $_ $p $a))
            (, (ancestor $p $a)))

; =============================================
;                 Test cases
; =============================================
(poi Ann)               ; test input
(solution Ann Bob)      ; desired outputs
(solution Ann Pam)
(solution Ann Tom)
(solution Ann Fred)

(poi Vic)
(solution Vic Whu)
(solution Vic Pam)      ; this is a mistake to showcase the example
; (solution Vic Zac)    ; this is a mistake to showcase the example

; =============================================
;                 Test code
; =============================================

; take the symmetric difference beween results and desired solutions
; MISTAKE = (ancestor U solution) \ (ancestor /\ solution)
(exec (3 0)
	(, (poi $p1) (ancestor $p1 $s1))
	(O (+ (MISTAKE $p1 $s1)))
)

(exec (3 0)
	(, (poi $p1) (solution $p1 $s1))
	(O (+ (MISTAKE $p1 $s1)))
)

(exec (3 1)
	(, (poi $p) (ancestor $p $s) (solution $p $s))
	(O (- (MISTAKE $p $s)))
)

; Optionally, we can also label when we got the correct answer
(exec (3 2)
    (, (poi $p))
    (, (CORRECT $p))
)

(exec (3 3)
     (, (MISTAKE $p $s))
     (O (- (CORRECT $p)))
)

Full program output

(poi Ann)
(poi Vic)
(CORRECT Ann)       ; <-------- test result
(child Ann Bob)
(child Bob Pam)
(child Bob Tom)
(child Jim Pat)
(child Liz Tom)
(child Ohm Uru)
(child Ohm Vic)
(child Pat Bob)
(child Tom Fred)
(child Uru Xey)
(child Uru Yip)
(child Vic Whu)
(child Vic Zac)
(parent Bob Ann)
(parent Bob Pat)
(parent Pam Bob)
(parent Pat Jim)
(parent Tom Bob)
(parent Tom Liz)
(parent Uru Ohm)
(parent Vic Ohm)
(parent Whu Vic)
(parent Xey Uru)
(parent Yip Uru)
(parent Zac Vic)
(parent Fred Tom)
(MISTAKE Vic Pam)       ; <-------- test result
(MISTAKE Vic Zac)       ; <-------- test result
(solution Ann Bob)
(solution Ann Pam)
(solution Ann Tom)
(solution Ann Fred)
(solution Vic Pam)
(solution Vic Whu)
(ancestor Ann Bob)
(ancestor Ann Pam)
(ancestor Ann Tom)
(ancestor Ann Fred)
(ancestor Vic Whu)
(ancestor Vic Zac)
(generation (S (S Z)) Ann Fred)
(generation (S Z) Ann Pam)
(generation (S Z) Ann Tom)
(generation Z Ann Bob)
(generation Z Vic Whu)
(generation Z Vic Zac)