How to Run the Verification Examples using the DMC System

SICStus Prolog must be installed.

1. Download the DMC system;

2. Download the dmc_patch.pl file (needed to run the liveness examples)

and place it in the "dmc" directory;

3. Run sicstus (from the "dmc" directory);

4. Load the DMC system by typing:

| ?- [demo].

5. Load the dmc_patch.pl file by typing:

| ?- [dmc_patch].

6. Load an example by typing:

| ?- ld(<filename>).

The verification examples should be stored in the "examples" directory

7. Run the DMC system by typing one of the following commands:

| ?- vn. %for safety properties (without abstraction)

| ?- va. %for safety properties (with abstraction)

| ?- ln. %for liveness properties (without abstraction)

| ?- lw. %for liveness properties (with abstraction)

| ?- ti. %to check whether a property holds (after completion of vn, va, ln, or lw)

| ?- ptime_ms(<command>). %to compute the running time of <command>.

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

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

[maurizio@proietti ~]$ cd dmc

[maurizio@proietti dmc]$ sicstus

SICStus 3.12.8 (x86-linux-glibc2.3): Tue May 8 13:30:29 CEST 2007

| ?- [demo].

% consulting /home/maurizio/DMC/dmc/demo.pl...

| ?- ld(bakery2_safety_DMC).

% consulting /home/maurizio/DMC/dmc/tmp/input_clp...

% consulted /home/maurizio/DMC/dmc/tmp/input_clp in module user, 0 msec 1776 bytes

yes

| ?- vn.

yes

| ?- ti.

Property satisfied

yes

| ?- ptime_ms(vn).

Execution time 20ms

yes

| ?- va.

yes

| ?- ptime_ms(va).

Execution time 50ms

yes

| ?- ti.

Property satisfied

yes

| ?-