| 1 | CIVL=civl
|
|---|
| 2 | VERIFY=$(CIVL) verify
|
|---|
| 3 |
|
|---|
| 4 | all: ring ring2 ring3 diffusion1d
|
|---|
| 5 |
|
|---|
| 6 | ring: ring.cvl mp_root.cvh mp_proc.cvh
|
|---|
| 7 | $(VERIFY) -inputNPROCS_BOUND=10 -inputN_BOUND=5 ring.cvl
|
|---|
| 8 |
|
|---|
| 9 | ring2: ring2.cvl mp_root2.cvh mp_proc2.cvh
|
|---|
| 10 | $(VERIFY) -inputNPROCS=3 -simplify=false ring2.cvl
|
|---|
| 11 |
|
|---|
| 12 | ring3: ring3.cvl
|
|---|
| 13 | $(VERIFY) ring3.cvl
|
|---|
| 14 |
|
|---|
| 15 | wildcard: wildcard.cvl
|
|---|
| 16 | $(VERIFY) wildcard.cvl
|
|---|
| 17 |
|
|---|
| 18 | wildcardBad: wildcardBad.cvl
|
|---|
| 19 | $(VERIFY) wildcardBad.cvl
|
|---|
| 20 |
|
|---|
| 21 | all: adder adderBad bank barrier barrier2 \
|
|---|
| 22 | barrierBad blockAdder blockAdderBad dining \
|
|---|
| 23 | diningBad locksBad locksBad10 locksGood \
|
|---|
| 24 | spawn spawn2 spawnBad
|
|---|
| 25 |
|
|---|
| 26 | adder: adder.cvl
|
|---|
| 27 | $(VERIFY) -inputB=5 adder.cvl
|
|---|
| 28 |
|
|---|
| 29 | adderBad: adderBad.cvl
|
|---|
| 30 | $(VERIFY) -inputB=4 -min adderBad.cvl
|
|---|
| 31 | $(CIVL) replay adderBad.cvl
|
|---|
| 32 |
|
|---|
| 33 | bank: bank.cvl
|
|---|
| 34 | $(VERIFY) -inputNUM_ACCOUNTS=3 bank.cvl
|
|---|
| 35 |
|
|---|
| 36 | barrier: barrier.cvl
|
|---|
| 37 | $(VERIFY) -inputB=4 barrier.cvl
|
|---|
| 38 |
|
|---|
| 39 | barrier2: barrier2.cvl
|
|---|
| 40 | $(VERIFY) -inputB=4 barrier2.cvl
|
|---|
| 41 |
|
|---|
| 42 | # Two kinds of violations are found in the following:
|
|---|
| 43 | # a deadlock, and an assertion violation:
|
|---|
| 44 | barrierBad: barrierBad.cvl
|
|---|
| 45 | $(VERIFY) -inputB=4 -min barrierBad.cvl
|
|---|
| 46 | $(CIVL) replay -id=0 barrierBad.cvl
|
|---|
| 47 | $(CIVL) replay -id=1 barrierBad.cvl
|
|---|
| 48 |
|
|---|
| 49 | blockAdder: blockAdder.cvl
|
|---|
| 50 | $(VERIFY) -inputB=6 -inputW=3 blockAdder.cvl
|
|---|
| 51 |
|
|---|
| 52 | blockAdderBad: blockAdderBad.cvl
|
|---|
| 53 | $(VERIFY) -inputB=6 -inputW=3 -min blockAdderBad.cvl
|
|---|
| 54 | $(CIVL) replay blockAdderBad.cvl
|
|---|
| 55 |
|
|---|
| 56 | dining: dining.cvl
|
|---|
| 57 | $(VERIFY) -inputB=4 dining.cvl
|
|---|
| 58 |
|
|---|
| 59 | diningBad:
|
|---|
| 60 | $(VERIFY) -inputB=4 -min diningBad.cvl
|
|---|
| 61 | $(CIVL) replay diningBad.cvl
|
|---|
| 62 |
|
|---|
| 63 | locksBad: locksBad.cvl
|
|---|
| 64 | $(VERIFY) locksBad.cvl
|
|---|
| 65 |
|
|---|
| 66 | locksBad10: locksBad10.cvl
|
|---|
| 67 | $(VERIFY) locksBad10.cvl
|
|---|
| 68 |
|
|---|
| 69 | locksGood: locksGood.cvl
|
|---|
| 70 | $(VERIFY) locksGood.cvl
|
|---|
| 71 |
|
|---|
| 72 | spawn: spawn.cvl
|
|---|
| 73 | $(VERIFY) -inputN=10 spawn.cvl
|
|---|
| 74 |
|
|---|
| 75 | spawn2: spawn2.cvl
|
|---|
| 76 | $(VERIFY) -inputN=10 spawn2.cvl
|
|---|
| 77 |
|
|---|
| 78 | spawnBad: spawnBad.cvl
|
|---|
| 79 | $(VERIFY) -inputN=10 spawnBad.cvl
|
|---|
| 80 |
|
|---|
