Added a few SAS example instances for testing.

This commit is contained in:
Patrick Lühne 2016-08-29 18:26:59 +02:00
parent 87717606b2
commit 9447912fbf
3 changed files with 4032 additions and 0 deletions

View File

@ -0,0 +1,921 @@
begin_version
3
end_version
begin_metric
0
end_metric
34
begin_variable
var0
-1
15
Atom airborne(airplane_cfbeg, seg_rwe_0_50)
Atom airborne(airplane_cfbeg, seg_rww_0_50)
Atom at-segment(airplane_cfbeg, seg_pp_0_60)
Atom at-segment(airplane_cfbeg, seg_ppdoor_0_40)
Atom at-segment(airplane_cfbeg, seg_rw_0_400)
Atom at-segment(airplane_cfbeg, seg_rwe_0_50)
Atom at-segment(airplane_cfbeg, seg_rww_0_50)
Atom at-segment(airplane_cfbeg, seg_twe1_0_200)
Atom at-segment(airplane_cfbeg, seg_twe2_0_50)
Atom at-segment(airplane_cfbeg, seg_twe3_0_50)
Atom at-segment(airplane_cfbeg, seg_twe4_0_50)
Atom at-segment(airplane_cfbeg, seg_tww1_0_200)
Atom at-segment(airplane_cfbeg, seg_tww2_0_50)
Atom at-segment(airplane_cfbeg, seg_tww3_0_50)
Atom at-segment(airplane_cfbeg, seg_tww4_0_50)
end_variable
begin_variable
var1
-1
2
Atom blocked(seg_pp_0_60, airplane_cfbeg)
NegatedAtom blocked(seg_pp_0_60, airplane_cfbeg)
end_variable
begin_variable
var2
-1
2
Atom blocked(seg_ppdoor_0_40, airplane_cfbeg)
NegatedAtom blocked(seg_ppdoor_0_40, airplane_cfbeg)
end_variable
begin_variable
var3
-1
2
Atom blocked(seg_rw_0_400, airplane_cfbeg)
NegatedAtom blocked(seg_rw_0_400, airplane_cfbeg)
end_variable
begin_variable
var4
-1
2
Atom blocked(seg_rwe_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_rwe_0_50, airplane_cfbeg)
end_variable
begin_variable
var5
-1
2
Atom blocked(seg_rwtw1_0_10, airplane_cfbeg)
NegatedAtom blocked(seg_rwtw1_0_10, airplane_cfbeg)
end_variable
begin_variable
var6
-1
2
Atom blocked(seg_rww_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_rww_0_50, airplane_cfbeg)
end_variable
begin_variable
var7
-1
2
Atom blocked(seg_twe1_0_200, airplane_cfbeg)
NegatedAtom blocked(seg_twe1_0_200, airplane_cfbeg)
end_variable
begin_variable
var8
-1
2
Atom blocked(seg_twe2_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_twe2_0_50, airplane_cfbeg)
end_variable
begin_variable
var9
-1
2
Atom blocked(seg_twe3_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_twe3_0_50, airplane_cfbeg)
end_variable
begin_variable
var10
-1
2
Atom blocked(seg_twe4_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_twe4_0_50, airplane_cfbeg)
end_variable
begin_variable
var11
-1
2
Atom blocked(seg_tww1_0_200, airplane_cfbeg)
NegatedAtom blocked(seg_tww1_0_200, airplane_cfbeg)
end_variable
begin_variable
var12
-1
2
Atom blocked(seg_tww2_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_tww2_0_50, airplane_cfbeg)
end_variable
begin_variable
var13
-1
2
Atom blocked(seg_tww3_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_tww3_0_50, airplane_cfbeg)
end_variable
begin_variable
var14
-1
2
Atom blocked(seg_tww4_0_50, airplane_cfbeg)
NegatedAtom blocked(seg_tww4_0_50, airplane_cfbeg)
end_variable
begin_variable
var15
-1
2
Atom facing(airplane_cfbeg, north)
Atom facing(airplane_cfbeg, south)
end_variable
begin_variable
var16
-1
14
Atom is-moving(airplane_cfbeg)
Atom is-parked(airplane_cfbeg, seg_pp_0_60)
Atom is-parked(airplane_cfbeg, seg_ppdoor_0_40)
Atom is-parked(airplane_cfbeg, seg_rw_0_400)
Atom is-parked(airplane_cfbeg, seg_rwe_0_50)
Atom is-parked(airplane_cfbeg, seg_rww_0_50)
Atom is-parked(airplane_cfbeg, seg_twe1_0_200)
Atom is-parked(airplane_cfbeg, seg_twe2_0_50)
Atom is-parked(airplane_cfbeg, seg_twe3_0_50)
Atom is-parked(airplane_cfbeg, seg_twe4_0_50)
Atom is-parked(airplane_cfbeg, seg_tww1_0_200)
Atom is-parked(airplane_cfbeg, seg_tww2_0_50)
Atom is-parked(airplane_cfbeg, seg_tww3_0_50)
Atom is-parked(airplane_cfbeg, seg_tww4_0_50)
end_variable
begin_variable
var17
1
2
Atom new-axiom@1(south, seg_ppdoor_0_40, seg_tww1_0_200, medium)
NegatedAtom new-axiom@1(south, seg_ppdoor_0_40, seg_tww1_0_200, medium)
end_variable
begin_variable
var18
1
2
Atom new-axiom@1(south, seg_rw_0_400, seg_rww_0_50, medium)
NegatedAtom new-axiom@1(south, seg_rw_0_400, seg_rww_0_50, medium)
end_variable
begin_variable
var19
1
2
Atom new-axiom@1(south, seg_tww1_0_200, seg_ppdoor_0_40, medium)
NegatedAtom new-axiom@1(south, seg_tww1_0_200, seg_ppdoor_0_40, medium)
end_variable
begin_variable
var20
1
2
Atom new-axiom@1(south, seg_tww1_0_200, seg_twe1_0_200, medium)
NegatedAtom new-axiom@1(south, seg_tww1_0_200, seg_twe1_0_200, medium)
end_variable
begin_variable
var21
-1
2
Atom occupied(seg_pp_0_60)
NegatedAtom occupied(seg_pp_0_60)
end_variable
begin_variable
var22
-1
2
Atom occupied(seg_ppdoor_0_40)
NegatedAtom occupied(seg_ppdoor_0_40)
end_variable
begin_variable
var23
-1
2
Atom occupied(seg_rw_0_400)
NegatedAtom occupied(seg_rw_0_400)
end_variable
begin_variable
var24
-1
2
Atom occupied(seg_rwe_0_50)
NegatedAtom occupied(seg_rwe_0_50)
end_variable
begin_variable
var25
-1
2
Atom occupied(seg_rww_0_50)
NegatedAtom occupied(seg_rww_0_50)
end_variable
begin_variable
var26
-1
2
Atom occupied(seg_twe1_0_200)
NegatedAtom occupied(seg_twe1_0_200)
end_variable
begin_variable
var27
-1
2
Atom occupied(seg_twe2_0_50)
NegatedAtom occupied(seg_twe2_0_50)
end_variable
begin_variable
var28
-1
2
Atom occupied(seg_twe3_0_50)
NegatedAtom occupied(seg_twe3_0_50)
end_variable
begin_variable
var29
-1
2
Atom occupied(seg_twe4_0_50)
NegatedAtom occupied(seg_twe4_0_50)
end_variable
begin_variable
var30
-1
2
Atom occupied(seg_tww1_0_200)
NegatedAtom occupied(seg_tww1_0_200)
end_variable
begin_variable
var31
-1
2
Atom occupied(seg_tww2_0_50)
NegatedAtom occupied(seg_tww2_0_50)
end_variable
begin_variable
var32
-1
2
Atom occupied(seg_tww3_0_50)
NegatedAtom occupied(seg_tww3_0_50)
end_variable
begin_variable
var33
-1
2
Atom occupied(seg_tww4_0_50)
NegatedAtom occupied(seg_tww4_0_50)
end_variable
4
begin_mutex_group
15
0 0
0 1
0 2
0 3
0 4
0 5
0 6
0 7
0 8
0 9
0 10
0 11
0 12
0 13
0 14
end_mutex_group
begin_mutex_group
13
0 2
0 3
0 4
0 5
0 6
0 7
0 8
0 9
0 10
0 11
0 12
0 13
0 14
end_mutex_group
begin_mutex_group
2
15 0
15 1
end_mutex_group
begin_mutex_group
14
16 0
16 1
16 2
16 3
16 4
16 5
16 6
16 7
16 8
16 9
16 10
16 11
16 12
16 13
end_mutex_group
begin_state
4
1
1
0
0
1
1
1
1
1
1
1
1
1
1
1
0
0
0
0
0
1
1
0
1
1
1
1
1
1
1
1
1
1
end_state
begin_goal
1
16 1
end_goal
43
begin_operator
move airplane_cfbeg medium north seg_pp_0_60 seg_ppdoor_0_40 north
2
15 0
16 0
5
0 0 2 3
0 1 -1 0
0 2 -1 0
0 21 -1 1
0 22 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium north seg_ppdoor_0_40 seg_tww1_0_200 south
2
16 0
17 1
8
0 0 3 11
0 1 -1 1
0 2 -1 0
0 7 -1 0
0 11 -1 0
0 15 0 1
0 22 -1 1
0 30 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium north seg_tww1_0_200 seg_ppdoor_0_40 south
2
16 0
19 1
8
0 0 11 3
0 2 -1 0
0 7 -1 0
0 11 -1 0
0 12 -1 1
0 15 0 1
0 22 -1 0
0 30 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium north seg_tww1_0_200 seg_twe1_0_200 south
2
16 0
20 1
8
0 0 11 7
0 2 -1 0
0 7 -1 0
0 11 -1 0
0 12 -1 1
0 15 0 1
0 26 -1 0
0 30 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium north seg_tww2_0_50 seg_tww1_0_200 north
2
15 0
16 0
6
0 0 12 11
0 11 -1 0
0 12 -1 0
0 13 -1 1
0 30 -1 0
0 31 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium north seg_tww3_0_50 seg_tww2_0_50 north
2
15 0
16 0
6
0 0 13 12
0 12 -1 0
0 13 -1 0
0 14 -1 1
0 31 -1 0
0 32 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium north seg_tww4_0_50 seg_tww3_0_50 north
2
15 0
16 0
7
0 0 14 13
0 5 -1 1
0 6 -1 1
0 13 -1 0
0 14 -1 0
0 32 -1 0
0 33 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_ppdoor_0_40 seg_pp_0_60 south
2
15 1
16 0
7
0 0 3 2
0 1 -1 0
0 2 -1 0
0 7 -1 1
0 11 -1 1
0 21 -1 0
0 22 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_rw_0_400 seg_rww_0_50 south
3
15 1
16 0
18 1
6
0 0 4 6
0 3 -1 0
0 4 -1 0
0 6 -1 0
0 23 -1 1
0 25 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_rwe_0_50 seg_rw_0_400 south
2
15 1
16 0
6
0 0 5 4
0 3 -1 0
0 4 -1 0
0 10 -1 1
0 23 -1 0
0 24 -1 1
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_rww_0_50 seg_tww4_0_50 north
1
16 0
9
0 0 6 14
0 3 -1 1
0 4 -1 1
0 5 -1 0
0 6 -1 0
0 14 -1 0
0 15 1 0
0 25 -1 1
0 33 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_twe1_0_200 seg_twe2_0_50 south
2
15 1
16 0
7
0 0 7 8
0 2 -1 1
0 7 -1 0
0 8 -1 0
0 11 -1 1
0 26 -1 1
0 27 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_twe2_0_50 seg_twe3_0_50 south
2
15 1
16 0
6
0 0 8 9
0 7 -1 1
0 8 -1 0
0 9 -1 0
0 27 -1 1
0 28 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_twe3_0_50 seg_twe4_0_50 south
2
15 1
16 0
6
0 0 9 10
0 8 -1 1
0 9 -1 0
0 10 -1 0
0 28 -1 1
0 29 -1 0
1
end_operator
begin_operator
move airplane_cfbeg medium south seg_twe4_0_50 seg_rwe_0_50 south
2
15 1
16 0
6
0 0 10 5
0 4 -1 0
0 9 -1 1
0 10 -1 0
0 24 -1 0
0 29 -1 1
1
end_operator
begin_operator
park airplane_cfbeg medium seg_pp_0_60 north
2
0 2
15 0
1
0 16 0 1
1
end_operator
begin_operator
park airplane_cfbeg medium seg_pp_0_60 south
2
0 2
15 1
2
0 2 -1 1
0 16 0 1
1
end_operator
begin_operator
park airplane_cfbeg medium seg_ppdoor_0_40 north
2
0 3
15 0
2
0 1 -1 1
0 16 0 2
1
end_operator
begin_operator
park airplane_cfbeg medium seg_ppdoor_0_40 south
2
0 3
15 1
3
0 7 -1 1
0 11 -1 1
0 16 0 2
1
end_operator
begin_operator
park airplane_cfbeg medium seg_rw_0_400 north
2
0 4
15 0
2
0 6 -1 1
0 16 0 3
1
end_operator
begin_operator
park airplane_cfbeg medium seg_rw_0_400 south
2
0 4
15 1
2
0 4 -1 1
0 16 0 3
1
end_operator
begin_operator
park airplane_cfbeg medium seg_rwe_0_50 north
2
0 5
15 0
3
0 3 -1 1
0 6 -1 1
0 16 0 4
1
end_operator
begin_operator
park airplane_cfbeg medium seg_rwe_0_50 south
2
0 5
15 1
2
0 10 -1 1
0 16 0 4
1
end_operator
begin_operator
park airplane_cfbeg medium seg_rww_0_50 north
2
0 6
15 0
2
0 14 -1 1
0 16 0 5
1
end_operator
begin_operator
park airplane_cfbeg medium seg_rww_0_50 south
2
0 6
15 1
3
0 3 -1 1
0 4 -1 1
0 16 0 5
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe1_0_200 north
2
0 7
15 0
2
0 8 -1 1
0 16 0 6
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe1_0_200 south
2
0 7
15 1
3
0 2 -1 1
0 11 -1 1
0 16 0 6
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe2_0_50 north
2
0 8
15 0
2
0 9 -1 1
0 16 0 7
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe2_0_50 south
2
0 8
15 1
2
0 7 -1 1
0 16 0 7
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe3_0_50 north
2
0 9
15 0
2
0 10 -1 1
0 16 0 8
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe3_0_50 south
2
0 9
15 1
2
0 8 -1 1
0 16 0 8
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe4_0_50 north
2
0 10
15 0
2
0 4 -1 1
0 16 0 9
1
end_operator
begin_operator
park airplane_cfbeg medium seg_twe4_0_50 south
2
0 10
15 1
2
0 9 -1 1
0 16 0 9
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww1_0_200 north
2
0 11
15 0
2
0 12 -1 1
0 16 0 10
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww1_0_200 south
2
0 11
15 1
3
0 2 -1 1
0 7 -1 1
0 16 0 10
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww2_0_50 north
2
0 12
15 0
2
0 13 -1 1
0 16 0 11
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww2_0_50 south
2
0 12
15 1
2
0 11 -1 1
0 16 0 11
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww3_0_50 north
2
0 13
15 0
2
0 14 -1 1
0 16 0 12
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww3_0_50 south
2
0 13
15 1
2
0 12 -1 1
0 16 0 12
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww4_0_50 north
2
0 14
15 0
3
0 5 -1 1
0 6 -1 1
0 16 0 13
1
end_operator
begin_operator
park airplane_cfbeg medium seg_tww4_0_50 south
2
0 14
15 1
2
0 13 -1 1
0 16 0 13
1
end_operator
begin_operator
takeoff airplane_cfbeg seg_rwe_0_50 south
1
15 1
16
0 0 5 0
0 1 -1 1
0 2 -1 1
0 3 -1 1
0 4 -1 1
0 5 -1 1
0 6 -1 1
0 7 -1 1
0 8 -1 1
0 9 -1 1
0 10 -1 1
0 11 -1 1
0 12 -1 1
0 13 -1 1
0 14 -1 1
0 24 -1 1
1
end_operator
begin_operator
takeoff airplane_cfbeg seg_rww_0_50 north
1
15 0
16
0 0 6 1
0 1 -1 1
0 2 -1 1
0 3 -1 1
0 4 -1 1
0 5 -1 1
0 6 -1 1
0 7 -1 1
0 8 -1 1
0 9 -1 1
0 10 -1 1
0 11 -1 1
0 12 -1 1
0 13 -1 1
0 14 -1 1
0 25 -1 1
1
end_operator
4
begin_rule
1
22 1
20 0 1
end_rule
begin_rule
1
24 1
18 0 1
end_rule
begin_rule
1
26 1
17 0 1
end_rule
begin_rule
1
26 1
19 0 1
end_rule

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,997 @@
begin_version
3
end_version
begin_metric
0
end_metric
29
begin_variable
var0
-1
14
Atom activate(philosopher-0, forks--pid-rfork)
Atom activate(philosopher-0, forks--pid-wfork)
Atom activate(philosopher-0, forks-__-pidp1__2_-rfork)
Atom activate(philosopher-0, forks-__-pidp1__2_-wfork)
Atom blocked-trans(philosopher-0, forks--pid-rfork)
Atom blocked-trans(philosopher-0, forks--pid-wfork)
Atom blocked-trans(philosopher-0, forks-__-pidp1__2_-rfork)
Atom blocked-trans(philosopher-0, forks-__-pidp1__2_-wfork)
Atom enabled(philosopher-0, forks--pid-rfork)
Atom enabled(philosopher-0, forks--pid-wfork)
Atom enabled(philosopher-0, forks-__-pidp1__2_-rfork)
Atom enabled(philosopher-0, forks-__-pidp1__2_-wfork)
Atom pending(philosopher-0)
<none of those>
end_variable
begin_variable
var1
-1
14
Atom activate(philosopher-1, forks--pid-rfork)
Atom activate(philosopher-1, forks--pid-wfork)
Atom activate(philosopher-1, forks-__-pidp1__2_-rfork)
Atom activate(philosopher-1, forks-__-pidp1__2_-wfork)
Atom blocked-trans(philosopher-1, forks--pid-rfork)
Atom blocked-trans(philosopher-1, forks--pid-wfork)
Atom blocked-trans(philosopher-1, forks-__-pidp1__2_-rfork)
Atom blocked-trans(philosopher-1, forks-__-pidp1__2_-wfork)
Atom enabled(philosopher-1, forks--pid-rfork)
Atom enabled(philosopher-1, forks--pid-wfork)
Atom enabled(philosopher-1, forks-__-pidp1__2_-rfork)
Atom enabled(philosopher-1, forks-__-pidp1__2_-wfork)
Atom pending(philosopher-1)
<none of those>
end_variable
begin_variable
var2
-1
4
Atom advance-head(forks-0-)
Atom advance-tail(forks-0-)
Atom settled(forks-0-)
<none of those>
end_variable
begin_variable
var3
-1
4
Atom advance-head(forks-1-)
Atom advance-tail(forks-1-)
Atom settled(forks-1-)
<none of those>
end_variable
begin_variable
var4
-1
5
Atom at-process(philosopher-0, state-1)
Atom at-process(philosopher-0, state-3)
Atom at-process(philosopher-0, state-4)
Atom at-process(philosopher-0, state-5)
Atom at-process(philosopher-0, state-6)
end_variable
begin_variable
var5
-1
5
Atom at-process(philosopher-1, state-1)
Atom at-process(philosopher-1, state-3)
Atom at-process(philosopher-1, state-4)
Atom at-process(philosopher-1, state-5)
Atom at-process(philosopher-1, state-6)
end_variable
begin_variable
var6
-1
2
Atom blocked(philosopher-0)
NegatedAtom blocked(philosopher-0)
end_variable
begin_variable
var7
-1
2
Atom blocked(philosopher-1)
NegatedAtom blocked(philosopher-1)
end_variable
begin_variable
var8
0
2
Atom new-axiom@0(philosopher-0, philosopher, state-1)
NegatedAtom new-axiom@0(philosopher-0, philosopher, state-1)
end_variable
begin_variable
var9
0
2
Atom new-axiom@0(philosopher-0, philosopher, state-3)
NegatedAtom new-axiom@0(philosopher-0, philosopher, state-3)
end_variable
begin_variable
var10
0
2
Atom new-axiom@0(philosopher-0, philosopher, state-4)
NegatedAtom new-axiom@0(philosopher-0, philosopher, state-4)
end_variable
begin_variable
var11
0
2
Atom new-axiom@0(philosopher-0, philosopher, state-5)
NegatedAtom new-axiom@0(philosopher-0, philosopher, state-5)
end_variable
begin_variable
var12
0
2
Atom new-axiom@0(philosopher-0, philosopher, state-6)
NegatedAtom new-axiom@0(philosopher-0, philosopher, state-6)
end_variable
begin_variable
var13
0
2
Atom new-axiom@0(philosopher-1, philosopher, state-1)
NegatedAtom new-axiom@0(philosopher-1, philosopher, state-1)
end_variable
begin_variable
var14
0
2
Atom new-axiom@0(philosopher-1, philosopher, state-3)
NegatedAtom new-axiom@0(philosopher-1, philosopher, state-3)
end_variable
begin_variable
var15
0
2
Atom new-axiom@0(philosopher-1, philosopher, state-4)
NegatedAtom new-axiom@0(philosopher-1, philosopher, state-4)
end_variable
begin_variable
var16
0
2
Atom new-axiom@0(philosopher-1, philosopher, state-5)
NegatedAtom new-axiom@0(philosopher-1, philosopher, state-5)
end_variable
begin_variable
var17
0
2
Atom new-axiom@0(philosopher-1, philosopher, state-6)
NegatedAtom new-axiom@0(philosopher-1, philosopher, state-6)
end_variable
begin_variable
var18
0
2
Atom new-axiom@1()
NegatedAtom new-axiom@1()
end_variable
begin_variable
var19
-1
2
Atom queue-head-msg(forks-0-, empty)
NegatedAtom queue-head-msg(forks-0-, empty)
end_variable
begin_variable
var20
-1
2
Atom queue-head-msg(forks-0-, fork)
NegatedAtom queue-head-msg(forks-0-, fork)
end_variable
begin_variable
var21
-1
2
Atom queue-head-msg(forks-1-, empty)
NegatedAtom queue-head-msg(forks-1-, empty)
end_variable
begin_variable
var22
-1
2
Atom queue-head-msg(forks-1-, fork)
NegatedAtom queue-head-msg(forks-1-, fork)
end_variable
begin_variable
var23
-1
2
Atom queue-msg(forks-0-, qs-0, fork)
NegatedAtom queue-msg(forks-0-, qs-0, fork)
end_variable
begin_variable
var24
-1
2
Atom queue-msg(forks-1-, qs-0, fork)
NegatedAtom queue-msg(forks-1-, qs-0, fork)
end_variable
begin_variable
var25
-1
2
Atom queue-size(forks-0-, one)
Atom queue-size(forks-0-, zero)
end_variable
begin_variable
var26
-1
2
Atom queue-size(forks-1-, one)
Atom queue-size(forks-1-, zero)
end_variable
begin_variable
var27
-1
2
Atom queue-tail-msg(forks-0-, fork)
NegatedAtom queue-tail-msg(forks-0-, fork)
end_variable
begin_variable
var28
-1
2
Atom queue-tail-msg(forks-1-, fork)
NegatedAtom queue-tail-msg(forks-1-, fork)
end_variable
10
begin_mutex_group
13
0 0
0 1
0 2
0 3
0 4
0 5
0 6
0 7
0 8
0 9
0 10
0 11
0 12
end_mutex_group
begin_mutex_group
9
0 0
0 1
0 2
0 3
0 8
0 9
0 10
0 11
0 12
end_mutex_group
begin_mutex_group
13
1 0
1 1
1 2
1 3
1 4
1 5
1 6
1 7
1 8
1 9
1 10
1 11
1 12
end_mutex_group
begin_mutex_group
9
1 0
1 1
1 2
1 3
1 8
1 9
1 10
1 11
1 12
end_mutex_group
begin_mutex_group
3
2 0
2 1
2 2
end_mutex_group
begin_mutex_group
3
3 0
3 1
3 2
end_mutex_group
begin_mutex_group
5
4 0
4 1
4 2
4 3
4 4
end_mutex_group
begin_mutex_group
5
5 0
5 1
5 2
5 3
5 4
end_mutex_group
begin_mutex_group
2
25 0
25 1
end_mutex_group
begin_mutex_group
2
26 0
26 1
end_mutex_group
begin_state
12
12
2
2
0
0
1
1
0
0
0
0
0
0
0
0
0
0
0
0
1
0
1
1
1
1
1
1
1
end_state
begin_goal
2
6 0
7 0
end_goal
56
begin_operator
activate-trans philosopher-0 philosopher forks--pid-rfork state-6 state-3
2
4 4
18 1
1
0 0 12 0
1
end_operator
begin_operator
activate-trans philosopher-0 philosopher forks--pid-wfork state-1 state-6
2
4 0
18 1
1
0 0 12 1
1
end_operator
begin_operator
activate-trans philosopher-0 philosopher forks--pid-wfork state-4 state-5
2
4 2
18 1
1
0 0 12 1
1
end_operator
begin_operator
activate-trans philosopher-0 philosopher forks-__-pidp1__2_-rfork state-3 state-4
2
4 1
18 1
1
0 0 12 2
1
end_operator
begin_operator
activate-trans philosopher-0 philosopher forks-__-pidp1__2_-wfork state-5 state-6
2
4 3
18 1
1
0 0 12 3
1
end_operator
begin_operator
activate-trans philosopher-1 philosopher forks--pid-rfork state-6 state-3
2
5 4
18 1
1
0 1 12 0
1
end_operator
begin_operator
activate-trans philosopher-1 philosopher forks--pid-wfork state-1 state-6
2
5 0
18 1
1
0 1 12 1
1
end_operator
begin_operator
activate-trans philosopher-1 philosopher forks--pid-wfork state-4 state-5
2
5 2
18 1
1
0 1 12 1
1
end_operator
begin_operator
activate-trans philosopher-1 philosopher forks-__-pidp1__2_-rfork state-3 state-4
2
5 1
18 1
1
0 1 12 2
1
end_operator
begin_operator
activate-trans philosopher-1 philosopher forks-__-pidp1__2_-wfork state-5 state-6
2
5 3
18 1
1
0 1 12 3
1
end_operator
begin_operator
advance-empty-queue-tail forks-0- queue-1 qs-0 qs-0 fork empty zero one
1
27 0
5
0 2 1 2
0 19 0 1
0 20 -1 0
0 23 -1 0
0 25 1 0
1
end_operator
begin_operator
advance-empty-queue-tail forks-0- queue-1 qs-0 qs-0 fork fork zero one
2
20 0
27 0
3
0 2 1 2
0 23 -1 0
0 25 1 0
1
end_operator
begin_operator
advance-empty-queue-tail forks-1- queue-1 qs-0 qs-0 fork empty zero one
1
28 0
5
0 3 1 2
0 21 0 1
0 22 -1 0
0 24 -1 0
0 26 1 0
1
end_operator
begin_operator
advance-empty-queue-tail forks-1- queue-1 qs-0 qs-0 fork fork zero one
2
22 0
28 0
3
0 3 1 2
0 24 -1 0
0 26 1 0
1
end_operator
begin_operator
advance-queue-head forks-0- queue-1 qs-0 qs-0 fork one zero
1
23 0
3
0 2 0 2
0 20 -1 0
0 25 0 1
1
end_operator
begin_operator
advance-queue-head forks-1- queue-1 qs-0 qs-0 fork one zero
1
24 0
3
0 3 0 2
0 22 -1 0
0 26 0 1
1
end_operator
begin_operator
block philosopher-0 state-1 philosopher
2
4 0
8 1
1
0 6 -1 0
1
end_operator
begin_operator
block philosopher-0 state-3 philosopher
2
4 1
9 1
1
0 6 -1 0
1
end_operator
begin_operator
block philosopher-0 state-4 philosopher
2
4 2
10 1
1
0 6 -1 0
1
end_operator
begin_operator
block philosopher-0 state-5 philosopher
2
4 3
11 1
1
0 6 -1 0
1
end_operator
begin_operator
block philosopher-0 state-6 philosopher
2
4 4
12 1
1
0 6 -1 0
1
end_operator
begin_operator
block philosopher-1 state-1 philosopher
2
5 0
13 1
1
0 7 -1 0
1
end_operator
begin_operator
block philosopher-1 state-3 philosopher
2
5 1
14 1
1
0 7 -1 0
1
end_operator
begin_operator
block philosopher-1 state-4 philosopher
2
5 2
15 1
1
0 7 -1 0
1
end_operator
begin_operator
block philosopher-1 state-5 philosopher
2
5 3
16 1
1
0 7 -1 0
1
end_operator
begin_operator
block philosopher-1 state-6 philosopher
2
5 4
17 1
1
0 7 -1 0
1
end_operator
begin_operator
block-read-queue-empty philosopher-0 forks--pid-rfork forks-0- fork zero
1
25 1
2
0 0 0 4
0 2 2 3
1
end_operator
begin_operator
block-read-queue-empty philosopher-0 forks-__-pidp1__2_-rfork forks-1- fork zero
1
26 1
2
0 0 2 6
0 3 2 3
1
end_operator
begin_operator
block-read-queue-empty philosopher-1 forks--pid-rfork forks-1- fork zero
1
26 1
2
0 1 0 4
0 3 2 3
1
end_operator
begin_operator
block-read-queue-empty philosopher-1 forks-__-pidp1__2_-rfork forks-0- fork zero
1
25 1
2
0 1 2 6
0 2 2 3
1
end_operator
begin_operator
block-read-wrong-message philosopher-0 forks--pid-rfork forks-0- fork empty
1
19 0
2
0 0 0 4
0 2 2 3
1
end_operator
begin_operator
block-read-wrong-message philosopher-0 forks-__-pidp1__2_-rfork forks-1- fork empty
1
21 0
2
0 0 2 6
0 3 2 3
1
end_operator
begin_operator
block-read-wrong-message philosopher-1 forks--pid-rfork forks-1- fork empty
1
21 0
2
0 1 0 4
0 3 2 3
1
end_operator
begin_operator
block-read-wrong-message philosopher-1 forks-__-pidp1__2_-rfork forks-0- fork empty
1
19 0
2
0 1 2 6
0 2 2 3
1
end_operator
begin_operator
block-write philosopher-0 forks--pid-wfork forks-0- queue-1 fork one
1
25 0
2
0 0 1 5
0 2 2 3
1
end_operator
begin_operator
block-write philosopher-0 forks-__-pidp1__2_-wfork forks-1- queue-1 fork one
1
26 0
2
0 0 3 7
0 3 2 3
1
end_operator
begin_operator
block-write philosopher-1 forks--pid-wfork forks-1- queue-1 fork one
1
26 0
2
0 1 1 5
0 3 2 3
1
end_operator
begin_operator
block-write philosopher-1 forks-__-pidp1__2_-wfork forks-0- queue-1 fork one
1
25 0
2
0 1 3 7
0 2 2 3
1
end_operator
begin_operator
perform-trans philosopher-0 philosopher forks--pid-rfork state-6 state-3
1
18 1
2
0 0 8 12
0 4 4 1
1
end_operator
begin_operator
perform-trans philosopher-0 philosopher forks--pid-wfork state-1 state-6
1
18 1
2
0 0 9 12
0 4 0 4
1
end_operator
begin_operator
perform-trans philosopher-0 philosopher forks--pid-wfork state-4 state-5
1
18 1
2
0 0 9 12
0 4 2 3
1
end_operator
begin_operator
perform-trans philosopher-0 philosopher forks-__-pidp1__2_-rfork state-3 state-4
1
18 1
2
0 0 10 12
0 4 1 2
1
end_operator
begin_operator
perform-trans philosopher-0 philosopher forks-__-pidp1__2_-wfork state-5 state-6
1
18 1
2
0 0 11 12
0 4 3 4
1
end_operator
begin_operator
perform-trans philosopher-1 philosopher forks--pid-rfork state-6 state-3
1
18 1
2
0 1 8 12
0 5 4 1
1
end_operator
begin_operator
perform-trans philosopher-1 philosopher forks--pid-wfork state-1 state-6
1
18 1
2
0 1 9 12
0 5 0 4
1
end_operator
begin_operator
perform-trans philosopher-1 philosopher forks--pid-wfork state-4 state-5
1
18 1
2
0 1 9 12
0 5 2 3
1
end_operator
begin_operator
perform-trans philosopher-1 philosopher forks-__-pidp1__2_-rfork state-3 state-4
1
18 1
2
0 1 10 12
0 5 1 2
1
end_operator
begin_operator
perform-trans philosopher-1 philosopher forks-__-pidp1__2_-wfork state-5 state-6
1
18 1
2
0 1 11 12
0 5 3 4
1
end_operator
begin_operator
queue-read philosopher-0 forks--pid-rfork forks-0- fork
1
20 0
8
0 0 0 8
1 1 4 1 -1 13
1 1 5 1 -1 13
1 1 6 1 -1 13
1 1 7 1 -1 13
0 2 2 0
0 6 -1 1
0 7 -1 1
1
end_operator
begin_operator
queue-read philosopher-0 forks-__-pidp1__2_-rfork forks-1- fork
1
22 0
8
0 0 2 10
1 1 4 1 -1 13
1 1 5 1 -1 13
1 1 6 1 -1 13
1 1 7 1 -1 13
0 3 2 0
0 6 -1 1
0 7 -1 1
1
end_operator
begin_operator
queue-read philosopher-1 forks--pid-rfork forks-1- fork
1
22 0
8
1 0 4 0 -1 13
1 0 5 0 -1 13
1 0 6 0 -1 13
1 0 7 0 -1 13
0 1 0 8
0 3 2 0
0 6 -1 1
0 7 -1 1
1
end_operator
begin_operator
queue-read philosopher-1 forks-__-pidp1__2_-rfork forks-0- fork
1
20 0
8
1 0 4 0 -1 13
1 0 5 0 -1 13
1 0 6 0 -1 13
1 0 7 0 -1 13
0 1 2 10
0 2 2 0
0 6 -1 1
0 7 -1 1
1
end_operator
begin_operator
queue-write philosopher-0 forks--pid-wfork forks-0- fork
0
9
0 0 1 9
1 1 4 1 -1 13
1 1 5 1 -1 13
1 1 6 1 -1 13
1 1 7 1 -1 13
0 2 2 1
0 6 -1 1
0 7 -1 1
0 27 -1 0
1
end_operator
begin_operator
queue-write philosopher-0 forks-__-pidp1__2_-wfork forks-1- fork
0
9
0 0 3 11
1 1 4 1 -1 13
1 1 5 1 -1 13
1 1 6 1 -1 13
1 1 7 1 -1 13
0 3 2 1
0 6 -1 1
0 7 -1 1
0 28 -1 0
1
end_operator
begin_operator
queue-write philosopher-1 forks--pid-wfork forks-1- fork
0
9
1 0 4 0 -1 13
1 0 5 0 -1 13
1 0 6 0 -1 13
1 0 7 0 -1 13
0 1 1 9
0 3 2 1
0 6 -1 1
0 7 -1 1
0 28 -1 0
1
end_operator
begin_operator
queue-write philosopher-1 forks-__-pidp1__2_-wfork forks-0- fork
0
9
1 0 4 0 -1 13
1 0 5 0 -1 13
1 0 6 0 -1 13
1 0 7 0 -1 13
0 1 3 11
0 2 2 1
0 6 -1 1
0 7 -1 1
0 27 -1 0
1
end_operator
11
begin_rule
1
0 4
12 0 1
end_rule
begin_rule
1
0 5
8 0 1
end_rule
begin_rule
1
0 5
10 0 1
end_rule
begin_rule
1
0 6
9 0 1
end_rule
begin_rule
1
0 7
11 0 1
end_rule
begin_rule
1
1 4
17 0 1
end_rule
begin_rule
1
1 5
13 0 1
end_rule
begin_rule
1
1 5
15 0 1
end_rule
begin_rule
1
1 6
14 0 1
end_rule
begin_rule
1
1 7
16 0 1
end_rule
begin_rule
2
2 2
3 2
18 0 1
end_rule