-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcro-srp-schedule.k
127 lines (100 loc) · 3.34 KB
/
cro-srp-schedule.k
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
/*
* This file is part of CRO-SRP-K.
*
* Copyright (C) 2012 Simon Aittamaa <[email protected]>.
*
* CRO-SRP-K is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* CRO-SRP-K is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with CRO-SRP-K. If not, see <http://www.gnu.org/licenses/>.
*/
require "cro-core-semantic.k"
/* ************************************************************************** */
require "cro-srp-config.k"
require "cro-srp-syntax.k"
/* ************************************************************************** */
module CRO-SRP-SCHEDULE
imports CRO-SRP-SYNTAX
imports CRO-SRP-CONFIG
/* ************************************************************************** */
syntax List ::= "enqueuByPriority" "(" Int "," Int "," K "," List ")"[function]
/* ************************************************************************** */
rule
enqueuByPriority(
P:Int,
C:Int,
Msg:K,
.List
) => (
ListItem(P, C, Msg)
.List
)
rule
enqueuByPriority(
P1:Int,
C1:Int,
Msg1:K,
ListItem(P2:Int, C2:Int, Msg2:K) T:List
) => (
ListItem(P1, C1, Msg1)
ListItem(P2, C2, Msg2)
T
)
when P1 >Int P2
rule
enqueuByPriority(
P1:Int,
C1:Int,
Msg1:K,
ListItem(P2:Int, C2:Int, Code2:K) T:List
) => (
ListItem(P2, C2, Code2) enqueuByPriority(P1, C1, Msg1, T)
)
when P1 <=Int P2
/* ************************************************************************** */
syntax K ::= "restorePriority" "(" ")"
/* ************************************************************************** */
rule
<k> restorePriority() => . ... </k>
<systempriority> ListItem(_:Int) => . ... </systempriority>
/* ************************************************************************** */
syntax K ::= "schedule" "(" ")"
/* ************************************************************************** */
rule
<k>
schedule() =>
Msg ~>
restorePriority()
...
</k>
<systempriority> (. => ListItem(P2:Int)) ListItem(P1:Int) ... </systempriority>
<systemceiling> ListItem(C1:Int) ... </systemceiling>
<messagequeue> ListItem(P2:Int, C2:Int, Msg:K) => . ... </messagequeue>
when (P2 >Int P1) andBool (C2 >Int C1) [transition]
rule
<k>
schedule() => .
...
</k>
<systempriority> ListItem(P1:Int) ... </systempriority>
<systemceiling> ListItem(C1:Int) ... </systemceiling>
<messagequeue> ListItem(P2:Int, C2:Int, _:K) ... </messagequeue>
when notBool((P2 >Int P1) andBool (C2 >Int C1)) [transition]
/* ************************************************************************** */
syntax K ::= "schedule" "(" Int "," Int "," Cmds ")"
/* ************************************************************************** */
rule
<k>
schedule(P:Int, C:Int, Msg:Cmds) => . ...
</k>
<messagequeue> Ms:List => enqueuByPriority(P, C, Msg, Ms) </messagequeue>
/* ************************************************************************** */
endmodule