From fe42e4b2a7fe539b518e44e9de84d562f03effc2 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 1 Mar 2016 21:27:32 +0100 Subject: [PATCH] up --- e42.smv | 38 ++++++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/e42.smv b/e42.smv index 91f16e7..c227d2a 100644 --- a/e42.smv +++ b/e42.smv @@ -6,14 +6,17 @@ ASSIGN next(state) := case state=none: case leftfork=inuse: none; - TRUE: left; + TRUE: {none, left}; esac; state=left: case - rightfork=inuse: left; - TRUE: both; +-- rightfork=inuse: left; + rightfork=inuse: {none, left}; +-- TRUE: {left, both}; + TRUE: {none, left, both}; esac; TRUE: none; esac; +JUSTICE state=both MODULE main VAR @@ -62,15 +65,22 @@ ASSIGN next(ph5.state)=both | next(ph0.state)=left | next(ph0.state)=both: inuse; TRUE: free; esac; +--This finds a deadlock LTLSPEC F( - G(ph0.state=left) | - G(ph1.state=left) | - G(ph2.state=left) | - G(ph3.state=left) | - G(ph4.state=left) | - G(ph5.state=left) | - G(ph6.state=left)) ---LTLSPEC G( --- (F (ph0.state=both)) & (F (ph1.state=both)) & (F (ph2.state=both)) & --- (F (ph3.state=both)) & (F (ph4.state=both)) & (F (ph5.state=both)) & --- (F (ph6.state=both))) + ph0.state=left & + ph1.state=left & + ph2.state=left & + ph3.state=left & + ph4.state=left & + ph5.state=left & + ph6.state=left) + +--Checks starvation +CTLSPEC AG( + (EF (ph0.state=both)) & + (EF (ph1.state=both)) & + (EF (ph2.state=both)) & + (EF (ph3.state=both)) & + (EF (ph4.state=both)) & + (EF (ph5.state=both)) & + (EF (ph6.state=both))) -- 2.20.1