| 1 | CIVL=civl
|
|---|
| 2 | VERIFY=$(CIVL) verify
|
|---|
| 3 |
|
|---|
| 4 | all: adder adderBad bank barrier barrier2 \
|
|---|
| 5 | barrierBad blockAdder blockAdderBad dining \
|
|---|
| 6 | diningBad locksBad locksBad10 locksGood \
|
|---|
| 7 | spawn spawn2 spawnBad
|
|---|
| 8 |
|
|---|
| 9 | adder: adder.cvl
|
|---|
| 10 | $(VERIFY) -inputB=5 adder.cvl
|
|---|
| 11 |
|
|---|
| 12 | adderBad: adderBad.cvl
|
|---|
| 13 | $(VERIFY) -inputB=4 -min adderBad.cvl
|
|---|
| 14 | $(CIVL) replay adderBad.cvl
|
|---|
| 15 |
|
|---|
| 16 | bank: bank.cvl
|
|---|
| 17 | $(VERIFY) -inputNUM_ACCOUNTS=3 bank.cvl
|
|---|
| 18 |
|
|---|
| 19 | barrier: barrier.cvl
|
|---|
| 20 | $(VERIFY) -inputB=4 barrier.cvl
|
|---|
| 21 |
|
|---|
| 22 | barrier2: barrier2.cvl
|
|---|
| 23 | $(VERIFY) -inputB=4 barrier2.cvl
|
|---|
| 24 |
|
|---|
| 25 | # Two kinds of violations are found in the following:
|
|---|
| 26 | # a deadlock, and an assertion violation:
|
|---|
| 27 | barrierBad: barrierBad.cvl
|
|---|
| 28 | $(VERIFY) -inputB=4 -min barrierBad.cvl
|
|---|
| 29 | $(CIVL) replay -id=0 barrierBad.cvl
|
|---|
| 30 | $(CIVL) replay -id=1 barrierBad.cvl
|
|---|
| 31 |
|
|---|
| 32 | blockAdder: blockAdder.cvl
|
|---|
| 33 | $(VERIFY) -inputB=6 -inputW=3 blockAdder.cvl
|
|---|
| 34 |
|
|---|
| 35 | blockAdderBad: blockAdderBad.cvl
|
|---|
| 36 | $(VERIFY) -inputB=6 -inputW=3 -min blockAdderBad.cvl
|
|---|
| 37 | $(CIVL) replay blockAdderBad.cvl
|
|---|
| 38 |
|
|---|
| 39 | dining: dining.cvl
|
|---|
| 40 | $(VERIFY) -inputB=4 dining.cvl
|
|---|
| 41 |
|
|---|
| 42 | diningBad:
|
|---|
| 43 | $(VERIFY) -inputB=4 -min diningBad.cvl
|
|---|
| 44 | $(CIVL) replay diningBad.cvl
|
|---|
| 45 |
|
|---|
| 46 | locksBad: locksBad.cvl
|
|---|
| 47 | $(VERIFY) locksBad.cvl
|
|---|
| 48 |
|
|---|
| 49 | locksBad10: locksBad10.cvl
|
|---|
| 50 | $(VERIFY) locksBad10.cvl
|
|---|
| 51 |
|
|---|
| 52 | locksGood: locksGood.cvl
|
|---|
| 53 | $(VERIFY) locksGood.cvl
|
|---|
| 54 |
|
|---|
| 55 | spawn: spawn.cvl
|
|---|
| 56 | $(VERIFY) -inputN=10 spawn.cvl
|
|---|
| 57 |
|
|---|
| 58 | spawn2: spawn2.cvl
|
|---|
| 59 | $(VERIFY) -inputN=10 spawn2.cvl
|
|---|
| 60 |
|
|---|
| 61 | spawnBad: spawnBad.cvl
|
|---|
| 62 | $(VERIFY) -inputN=10 spawnBad.cvl
|
|---|
| 63 |
|
|---|
| 64 | clean:
|
|---|
| 65 | rm -rf CIVLREP *~
|
|---|
| 66 |
|
|---|
