Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
i7
peregrine
Commits
fe0a30e3
Commit
fe0a30e3
authored
Jul 28, 2014
by
Philipp Meyer
Browse files
Tested termination by reachability on example
parent
85d7db33
Changes
4
Hide whitespace changes
Inline
Side-by-side
examples/h_fairly_terminates.pnet.terminating
0 → 100644
View file @
fe0a30e3
PLACE 'sigma,'m1,'m2,x,not_x,scheduler,h,g,pending_h,pending_g,'x,'not_x,'scheduler,'h,'g,'pending_h,'pending_g,dg_out,dh_out;
MARKING 'm1:1,'pending_h:1,'scheduler:1,'x:1,pending_h:1,scheduler:1,x:1;
TRANSITION 'switch
CONSUME 'm1:1;
PRODUCE 'm2:1;
TRANSITION dh
CONSUME 'scheduler:1,'pending_h:1,scheduler:1,pending_h:1,'m1:1;
PRODUCE 'h:1,h:1,'m1:1;
TRANSITION 'dh
CONSUME 'scheduler:1,'pending_h:1,'m2:1;
PRODUCE 'h:1,'sigma:1,'m2:1,dh_out:1;
TRANSITION dg
CONSUME 'scheduler:1,'pending_g:1,scheduler:1,pending_g:1,'m1:1;
PRODUCE 'g:1,g:1,'m1:1;
TRANSITION 'dg
CONSUME 'scheduler:1,'pending_g:1,'m2:1;
PRODUCE 'g:1,'sigma:1,'m2:1,dg_out:1;
TRANSITION ht
CONSUME 'h:1,'x:1,h:1,x:1,'m1:1;
PRODUCE 'x:1,'pending_h:1,'pending_g:1,'scheduler:1,x:1,pending_h:1,pending_g:1,scheduler:1,'m1:1;
TRANSITION 'ht
CONSUME 'h:1,'x:1,'m2:1;
PRODUCE 'x:1,'pending_h:1,'pending_g:1,'scheduler:1,'sigma:1,'m2:1;
TRANSITION hf
CONSUME 'h:1,'not_x:1,h:1,not_x:1,'m1:1;
PRODUCE 'not_x:1,'scheduler:1,not_x:1,scheduler:1,'m1:1;
TRANSITION 'hf
CONSUME 'h:1,'not_x:1,'m2:1;
PRODUCE 'not_x:1,'scheduler:1,'sigma:1,'m2:1;
TRANSITION gt
CONSUME 'g:1,'x:1,g:1,x:1,'m1:1;
PRODUCE 'not_x:1,'scheduler:1,not_x:1,scheduler:1,'m1:1;
TRANSITION 'gt
CONSUME 'g:1,'x:1,'m2:1;
PRODUCE 'not_x:1,'scheduler:1,'sigma:1,'m2:1;
TRANSITION gf
CONSUME 'g:1,'not_x:1,g:1,not_x:1,'m1:1;
PRODUCE 'not_x:1,'scheduler:1,not_x:1,scheduler:1,'m1:1;
TRANSITION 'gf
CONSUME 'g:1,'not_x:1,'m2:1;
PRODUCE 'not_x:1,'scheduler:1,'sigma:1,'m2:1;
examples/h_fairly_terminates.pnet.terminating.sara
0 → 100644
View file @
fe0a30e3
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE h_fairly_terminates.pnet.terminating TYPE LOLA;
INITIAL 'm1:1,'pending_h:1,'scheduler:1,'x:1,pending_h:1,scheduler:1,x:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,dh_out>1,dg_out>1,'x+-1x>0,'not_x+-1not_x>0,'scheduler+-1scheduler>0,'h+-1h>0,'g+-1g>0,'pending_h+-1pending_h>0,'pending_g+-1pending_g>0;
examples/h_fairly_terminates.pnet.terminating.task1
0 → 100644
View file @
fe0a30e3
EF ('sigma >= 1 AND dh_out >= 1 AND dg_out >= 1 AND ('x - x) >= 0 AND ('not_x - not_x) >= 0 AND ('scheduler - scheduler) >= 0 AND ('h - h) >= 0 AND ('g - g) >= 0 AND ('pending_h - pending_h) >= 0 AND ('pending_g - pending_g) >= 0)
examples/h_fairly_terminates_by_reachability.pnet
0 → 100644
View file @
fe0a30e3
petri net "asynchronous program" {
places {
// State
x not_x x_ not_x_
// Scheduler
scheduler scheduler_
// Handlers
h g h_ g_
// Pending instances
pending_h pending_g pending_h_ pending_g_
m1 m2 dh_out dg_out
}
transitions {
dh dg ht hf gt gf
dh_ dg_ ht_ hf_ gt_ gf_
switch
}
arcs {
// Dispatch h
{ scheduler, pending_h, scheduler_, pending_h_, m1 } -> dh -> { h, h_, m1 }
{ scheduler_, pending_h_, m2 } -> dh_ -> { h_, m2, dh_out }
// Dispatch g
{ scheduler, pending_g, scheduler_, pending_g_, m1 } -> dg -> { g, g_, m1 }
{ scheduler_, pending_g_, m2 } -> dg_ -> { g_, m2, dg_out }
// Exit h if x == true
{ h, x, h_, x_, m1 } -> ht -> { x, pending_h, pending_g, scheduler, x_, pending_h_, pending_g_, scheduler_, m1 }
{ h_, x_, m2 } -> ht_ -> { x_, pending_h_, pending_g_, scheduler_, m2 }
// Exit h if x == false
{ h, not_x, h_, not_x_, m1 } -> hf -> { not_x, scheduler, not_x_, scheduler_, m1 }
{ h_, not_x_, m2 } -> hf_ -> { not_x_, scheduler_, m2 }
// Exit g if x == true
{ g, x, g_, x_, m1 } -> gt -> { not_x, scheduler, not_x_, scheduler_, m1 }
{ g_, x_, m2 } -> gt_ -> { not_x_, scheduler_, m2 }
// Exit g if x == false
{ g, not_x, g_, not_x_, m1 } -> gf -> { not_x, scheduler, not_x_, scheduler_, m1 }
{ g_, not_x_, m2 } -> gf_ -> { not_x_, scheduler_, m2 }
m1 -> switch -> m2
}
initial {
// Initially, x is true, there's one pending instance of h(),
// and the scheduler has control.
x pending_h scheduler
x_ pending_h_ scheduler_
m1
}
}
safety property "terminating" {
dh_out >= 1 && dg_out >= 1 &&
x_ >= x && not_x_ >= not_x &&
scheduler_ >= scheduler &&
h_ >= h && g_ >= g &&
pending_h_ >= pending_h && pending_g_ >= pending_g
}
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment