How to Run the Verification Examples using the MAP System

SICStus Prolog must be installed.

1. Run sicstus (from the MAPline directory)

2. Load the MAP system by typing:

| ?- [make_map]. (under Linux) or

| ?- [make_map_w]. (under Windows)

3. Load the Unfold/Fold model checker by typing:

| ?- ufmc.

4. Load an example by typing:

| ?- st.

and selecting a file from the list.

The verification examples should be stored in the "MAPline/Progs" directory

5. Verify a property by typing:

| ?- verify.

and then

|: safe. for safety properties, or

|: starvfree. for liveness properties

See below for an example.

More details on the MAP system can be found on the MAP page.

%-------------- other commands:

| ?- dtrace(on).

%Transformation steps are visualized during derivation

| ?- dtrace(off).

%Transformation steps are not visualized during derivation

| ?- cvs.

%to change settings.

| ?- svs.

%to show current settings.

%------------------ Example ------------------

| ?- [make_map_w]. %Under Windows

% consulting c:/documents and settings/maurizio/desktop/mapline/make_map_w.pl...

| ?- ufmc.

% compiling c:/documents and settings/maurizio/desktop/mapline/src_sics/ufmc.pl...

current verification settings:

[prog_maxcoeff(off),less(maxcoeff),gen(widen),widen(e_leq_maxcoeff)]

cvs to change settings.

svs to show current settings.

yes

| ?- st.

Choose program:

1 ) bakery2_map.pl

2 ) bakery3_map.pl

3 ) berkeley_map.pl

4 ) dragon_map.pl

5 ) firefly_map.pl

6 ) futurebus_map.pl

7 ) illinois_map.pl

8 ) mesi_map.pl

9 ) moesi_map.pl

10 ) resetpetrinet_map.pl

11 ) running_map.pl

12 ) synapse_map.pl

13 ) ticket_map.pl

Initial program [no selection]: 12

Initial program:

1. t(s(A,B,C),s(A,B,C)) :- A>=0, B>=0, C>=0, C+B>=1.

2. t(s(A,B,C),s(D,E,F)) :- B>=0, C>=0, A>=1, D=:=A+C-1, E=:=B+1, F=:=0.

3. t(s(A,B,C),s(A,B,C)) :- A>=0, B>=0, C>=1.

4. t(s(A,B,C),s(D,E,F)) :- A>=0, C>=0, B>=1, D=:=A+C+B-1, E=:=0, F=:=1.

5. t(s(A,B,C),s(D,E,F)) :- B>=0, C>=0, A>=1, D=:=A+C+B-1, E=:=0, F=:=1.

6. elem(s(A,B,C),initial) :- A>=0, B=:=0, C=:=0.

7. elem(s(A,B,C),unsafe1) :- A>=0, B>=1, C>=1.

8. elem(s(A,B,C),unsafe2) :- A>=0, B>=0, C>=2.

9. safe :- prop(not(ef(or(unsafe1,unsafe2)))).

10. safe1 :- prop(not(ef(unsafe1))).

11. safe2 :- prop(not(ef(unsafe2))).

yes

| ?- verify.

enter a property

|: safe.

---specialization strategy---

#definitions: 7

---post remove-unfold strategy---

true

Elapsed time 16ms

yes