mirror of
https://github.com/bluekitchen/btstack.git
synced 2025-04-16 08:42:28 +00:00
extract StateMachineExtration as seperate project
This commit is contained in:
Matthias Ringwald
parent
7102391c2a
commit
e14ac1dfae
@ -1,31 +0,0 @@
|
|||||||
|
|
||||||
Project title: "Annotation-based state machine definition for doubly nested switch-case implementations"
|
|
||||||
|
|
||||||
- goals: testability, documentation
|
|
||||||
- assumptions: fixed code stucture
|
|
||||||
- input: some code (.c)
|
|
||||||
- output: graphviz state machine ...
|
|
||||||
- documentation: BTstack Wiki page
|
|
||||||
- implementation: Python
|
|
||||||
- problems:
|
|
||||||
- implicit event like "can send packet now", =? deal with guards?
|
|
||||||
- "inverse handler" for "global" events
|
|
||||||
|
|
||||||
Example:
|
|
||||||
{
|
|
||||||
// @STATEMACHINE(multiplexer)
|
|
||||||
switch (multiplexer->state) { // detect state variable, count {
|
|
||||||
case W4_MULTIPLEXER: // implicit state
|
|
||||||
switch (event) { // events start here
|
|
||||||
case L2CAP_OPEN: // implicit event
|
|
||||||
// @ACTION(action description)
|
|
||||||
multiplexer->state = OTHER_STATE;
|
|
||||||
break; // break || return -> end case block
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case OTHER_STATE:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
104
docs/extract.py
104
docs/extract.py
@ -1,104 +0,0 @@
|
|||||||
#!/usr/bin/env python
|
|
||||||
|
|
||||||
import re
|
|
||||||
|
|
||||||
class Transition(object):
|
|
||||||
def __init__ (self, fromState, toState, event, guard, action):
|
|
||||||
self.fromState = fromState
|
|
||||||
self.toState = toState
|
|
||||||
self.event = event
|
|
||||||
self.guard = guard
|
|
||||||
self.action = action
|
|
||||||
|
|
||||||
statemachineName = ""
|
|
||||||
stateVariable = ""
|
|
||||||
numBraces = 0
|
|
||||||
fromState = ""
|
|
||||||
toState = ""
|
|
||||||
onEvent = ""
|
|
||||||
action = ""
|
|
||||||
|
|
||||||
def parseLine(line):
|
|
||||||
global statemachineName
|
|
||||||
global numBraces
|
|
||||||
global stateVariable
|
|
||||||
global fromState
|
|
||||||
global toState
|
|
||||||
global onEvent
|
|
||||||
global action
|
|
||||||
|
|
||||||
# looks for annotations
|
|
||||||
ann = re.compile("(@\w*)\s*(\((.*)\))?")
|
|
||||||
anns = ann.findall(line)
|
|
||||||
if anns:
|
|
||||||
if "@STATEMACHINE" in anns[0]:
|
|
||||||
# print "statemachine, name:", anns[0][2]
|
|
||||||
statemachineName = anns[0][2]
|
|
||||||
numBraces = 0
|
|
||||||
stateVariable = ""
|
|
||||||
if "@ACTION" in anns[0]:
|
|
||||||
action = anns[0][2]
|
|
||||||
|
|
||||||
# look for switch
|
|
||||||
switch = re.compile("(switch)\s*\(\s*(.*)\s*\)")
|
|
||||||
switches = switch.findall(line)
|
|
||||||
if (switches):
|
|
||||||
if numBraces == 0:
|
|
||||||
stateVariable = switches[0][1]
|
|
||||||
# print "switch on state opened", numBraces, stateVariable
|
|
||||||
# if numBraces == 1:
|
|
||||||
# print "switch on event opened", numBraces
|
|
||||||
|
|
||||||
# count curly braces when inside statemachine
|
|
||||||
if statemachineName:
|
|
||||||
for c in line:
|
|
||||||
before = numBraces
|
|
||||||
if '{' in c:
|
|
||||||
numBraces = numBraces + 1
|
|
||||||
if '}' in c:
|
|
||||||
numBraces = numBraces - 1
|
|
||||||
|
|
||||||
# look for case
|
|
||||||
case = re.compile("(case)\s*(.*):")
|
|
||||||
cases = case.findall(line)
|
|
||||||
if cases:
|
|
||||||
if numBraces == 1:
|
|
||||||
# print "from state: " + cases[0][1]
|
|
||||||
fromState = cases[0][1]
|
|
||||||
if numBraces == 2:
|
|
||||||
# print "on event: " + cases[0][1]
|
|
||||||
onEvent = cases[0][1]
|
|
||||||
toState = ""
|
|
||||||
action = ""
|
|
||||||
|
|
||||||
# look for break or return
|
|
||||||
brk = re.compile("(break)")
|
|
||||||
breaks = brk.findall(line)
|
|
||||||
rtrn = re.compile("(return)")
|
|
||||||
returns = rtrn.findall(line)
|
|
||||||
if numBraces > 1:
|
|
||||||
if breaks or returns:
|
|
||||||
if not toState:
|
|
||||||
toState = fromState
|
|
||||||
# print "to state:", toState
|
|
||||||
print fromState + "->" + toState + " [label=\"" + onEvent + "/" + action + "\"];"
|
|
||||||
|
|
||||||
# look for state transition
|
|
||||||
if stateVariable:
|
|
||||||
stateTransition = re.compile( stateVariable + "\s*=\s*(.*);")
|
|
||||||
transition = stateTransition.findall(line)
|
|
||||||
if transition:
|
|
||||||
toState = transition[0]
|
|
||||||
|
|
||||||
|
|
||||||
def parseFile(filename):
|
|
||||||
f = open (filename, "r")
|
|
||||||
for line in f:
|
|
||||||
parseLine(line)
|
|
||||||
f.close()
|
|
||||||
|
|
||||||
print "digraph fsm { "
|
|
||||||
print "size = \"8.5\""
|
|
||||||
parseFile("/Projects/iPhone/btstack/src/l2cap.c")
|
|
||||||
print "}"
|
|
||||||
|
|
||||||
@ -1,57 +0,0 @@
|
|||||||
digraph l2cap {
|
|
||||||
// rankdir=LR;
|
|
||||||
size="8,5"
|
|
||||||
// orientation=landscape;
|
|
||||||
// rotate = 90;
|
|
||||||
|
|
||||||
OPEN [shape=doublecircle];
|
|
||||||
CLOSE [shape=doublecircle];
|
|
||||||
|
|
||||||
// DISCONNECT_REQUEST handling for non-open state
|
|
||||||
// WAIT_CONNECT_RSP->WILL_SEND_DISCONNECT_RESPONSE [label = "RECEIVED DISCONNECT_REQUEST"];
|
|
||||||
// WAIT_CONFIG_REQ_OR_SEND_CONFIG_REQ->WILL_SEND_DISCONNECT_RESPONSE [label = "DISCONNECTION_REQUEST"];
|
|
||||||
// WAIT_CONFIG_REQ_RSP_OR_CONFIG_REQ->WILL_SEND_DISCONNECT_RESPONSE [ label = "RECVEIVED DISCONNECTION_REQUEST"];
|
|
||||||
// WAIT_CONFIG_REQ->WILL_SEND_DISCONNECT_RESPONSE [label = "RECEIVED DISCONNECTION_REQUEST"];
|
|
||||||
// WAIT_CONFIG_REQ_RSP->WILL_SEND_DISCONNECT_RESPONSE [label = "RECEIVED DISCONNECTION_REQUEST"];
|
|
||||||
// WAIT_DISCONNECT->WILL_SEND_DISCONNECT_RESPONSE [label = "RECEIVED DISCONNECT_REQUEST"];
|
|
||||||
|
|
||||||
// l2cap_run
|
|
||||||
WILL_SEND_CREATE_CONNECTION -> WAIT_CONNECTION_COMPLETE [label = "SEND CREATE CONNECTION"];
|
|
||||||
WILL_SEND_CONNECTION_RESPONSE_DECLINE -> CLOSE [label = "SEND CONNECTION_RESPONSE ERR"];
|
|
||||||
WILL_SEND_CONNECTION_RESPONSE_ACCEPT -> CONFIG [label = "SEND CONNECTION_RESPONSE OK"];
|
|
||||||
WILL_SEND_CONNECTION_REQUEST -> WAIT_CONNECT_RSP [label = "SEND CONNECTION_REQUEST"];
|
|
||||||
|
|
||||||
WILL_SEND_DISCONNECT_RESPONSE -> CLOSE [ label = "SEND DISCONNECTION_RESPONSE"];
|
|
||||||
WILL_SEND_DISCONNECT_REQUEST -> WAIT_DISCONNECT [label = "SEND DISCONNECTION_REQUEST"];
|
|
||||||
|
|
||||||
// l2cap_create_channel_internal
|
|
||||||
CLOSE -> WILL_SEND_CREATE_CONNECTION [label = "l2cap create channel internal"];
|
|
||||||
|
|
||||||
// l2cap_disconnect_internal
|
|
||||||
OPEN -> WILL_SEND_DISCONNECT_REQUEST [label = "l2cap disconnect internal"];
|
|
||||||
|
|
||||||
// l2cap_handle_connection_success_for_addr
|
|
||||||
WAIT_CONNECTION_COMPLETE->WILL_SEND_CONNECTION_REQUEST [ label = "outgoing,baseband open"];
|
|
||||||
|
|
||||||
// l2cap_handle_disconnect_request
|
|
||||||
OPEN -> WILL_SEND_DISCONNECT_RESPONSE [label = "RECEIVED DISCONNECT_REQUEST"];
|
|
||||||
|
|
||||||
// l2cap_handle_connection_request
|
|
||||||
CLOSE -> WAIT_CLIENT_ACCEPT_OR_REJECT [label = "RECEIVED CONNECTION REQUEST"];
|
|
||||||
|
|
||||||
// l2cap_accept_connection_internal
|
|
||||||
WAIT_CLIENT_ACCEPT_OR_REJECT -> WILL_SEND_CONNECTION_RESPONSE_ACCEPT [ label = "l2cap accept internal"];
|
|
||||||
|
|
||||||
// l2cap_decline_connection_internal
|
|
||||||
WAIT_CLIENT_ACCEPT_OR_REJECT -> WILL_SEND_CONNECTION_RESPONSE_DECLINE [ label = "l2cap decline internal"];
|
|
||||||
|
|
||||||
// l2cap_signaling_handler_channel
|
|
||||||
WAIT_CONNECT_RSP->CONFIG [ label = "CONNECTION_RESPONSE OK"];
|
|
||||||
WAIT_CONNECT_RSP->CLOSE [label = "CONNECTION_RESPONSE ERR"];
|
|
||||||
WAIT_DISCONNECT->CLOSE [label = "RECEIVED DISCONNECT_RESPONSE"];
|
|
||||||
CONFIG->OPEN [label="RCVD CONF RSP && SENT CONF RSP"];
|
|
||||||
CONFIG->CONFIG[label="send and respond CONF REQ"];
|
|
||||||
|
|
||||||
// l2cap_close_connection
|
|
||||||
OPEN->WILL_SEND_DISCONNECT_REQUEST [label = "client closed"];
|
|
||||||
}
|
|
||||||
54
docs/lamp.c
54
docs/lamp.c
@ -1,54 +0,0 @@
|
|||||||
#include <stdio.h>
|
|
||||||
|
|
||||||
typedef enum {
|
|
||||||
LAMP_OFF = 1,
|
|
||||||
LAMP_ON
|
|
||||||
} state_t;
|
|
||||||
|
|
||||||
typedef enum {
|
|
||||||
TOGGLE_ON = 1,
|
|
||||||
TOGGLE_OFF
|
|
||||||
} event_t;
|
|
||||||
|
|
||||||
state_t state;
|
|
||||||
|
|
||||||
void statemachine(event_t ev){
|
|
||||||
|
|
||||||
printf("State: %u, event: %u\n", state, ev);
|
|
||||||
|
|
||||||
// @STATEMACHINE(lamp)
|
|
||||||
switch(state){
|
|
||||||
case LAMP_OFF:
|
|
||||||
switch(ev){
|
|
||||||
case TOGGLE_ON:
|
|
||||||
// @ACTION(Turning lamp on)
|
|
||||||
printf("Turning lamp on\n");
|
|
||||||
state = LAMP_ON;
|
|
||||||
break;
|
|
||||||
case TOGGLE_OFF:
|
|
||||||
// @ACTION(Ignoring toggle off)
|
|
||||||
printf("Ignoring toggle off\n");
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case LAMP_ON:
|
|
||||||
switch(ev){
|
|
||||||
case TOGGLE_ON:
|
|
||||||
// @ACTION(Ignoring toggle on)
|
|
||||||
printf("Ignoring toggle on\n");
|
|
||||||
break;
|
|
||||||
case TOGGLE_OFF:
|
|
||||||
// @ACTION(Turning lamp off)
|
|
||||||
printf("Turning lamp off\n");
|
|
||||||
state = LAMP_OFF;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
int main(void){
|
|
||||||
state = LAMP_OFF;
|
|
||||||
statemachine( TOGGLE_ON );
|
|
||||||
statemachine( TOGGLE_ON );
|
|
||||||
statemachine( TOGGLE_OFF );
|
|
||||||
}
|
|
||||||
@ -1,44 +0,0 @@
|
|||||||
digraph rfcomm_channel {
|
|
||||||
// rankdir=LR;
|
|
||||||
size="8,5"
|
|
||||||
// orientation=landscape;
|
|
||||||
// rotate = 90;
|
|
||||||
|
|
||||||
CLOSED [shape=doublecircle];
|
|
||||||
OPEN [shape=doublecircle];
|
|
||||||
|
|
||||||
// DISC #x or DM
|
|
||||||
|
|
||||||
// rfcomm_create_channel_internal
|
|
||||||
CLOSED->W4_MULTIPLEXER [label = "create channel [multiplexer==closed]"];
|
|
||||||
CLOSED->SEND_UIH_PN [label = "create channel [multiplexer==open]"];
|
|
||||||
W4_MULTIPLEXER->SEND_UIH_PN [label = "multiplexere opened"];
|
|
||||||
SEND_UIH_PN->W4_PN_RSP [label="SEND PN CMD"];
|
|
||||||
W4_PN_RSP->SEND_SABM_W4_UA [label="RECV PN RSP"];
|
|
||||||
SEND_SABM_W4_UA->W4_UA[label="SEND SABM"];
|
|
||||||
|
|
||||||
// rfcomm_multiplexer_l2cap_packet_handler
|
|
||||||
|
|
||||||
// rfcomm_packet_handler
|
|
||||||
CLOSED->INCOMING_SETUP [label = "RECV SABM#x / inform client"];
|
|
||||||
CLOSED->INCOMING_SETUP [label = "RECV PN CMD / inform client"];
|
|
||||||
CLOSED->INCOMING_SETUP [label = "RECV RPN CMD / inform client"];
|
|
||||||
|
|
||||||
// rfcomm_decline_connection_internal
|
|
||||||
INCOMING_SETUP->SEND_DM [label = "decline connection"];
|
|
||||||
|
|
||||||
// rfcomm_disconnect_internal
|
|
||||||
OPEN->SEND_DISC [label="disconnect"];
|
|
||||||
|
|
||||||
// rfcomm_run
|
|
||||||
SEND_DM->CLOSED [label="SEND DM_PF"];
|
|
||||||
SEND_DISC->CLOSED [label="SEND DISC"];
|
|
||||||
|
|
||||||
// rfcomm_accept_connection_internal
|
|
||||||
INCOMING_SETUP->INCOMING_SETUP [label="accept connection/confirm"];
|
|
||||||
INCOMING_SETUP->DLC_SETUP [label="-[CAN SEND] / SEND UA"];
|
|
||||||
W4_UA->DLC_SETUP[label="RECV UA"];
|
|
||||||
DLC_SETUP->OPEN [label="exchanged MSC & credits > 0"];
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
@ -1,21 +0,0 @@
|
|||||||
digraph rfcomm_multiplexer {
|
|
||||||
// rankdir=LR;
|
|
||||||
size="8,5"
|
|
||||||
// orientation=landscape;
|
|
||||||
// rotate = 90;
|
|
||||||
|
|
||||||
CLOSED [shape=doublecircle];
|
|
||||||
OPEN [shape=doublecircle];
|
|
||||||
|
|
||||||
CLOSED->W4_CONNECT [label = "create_channel outgoing"];
|
|
||||||
W4_CONNECT->SEND_SABM_0 [label = "l2cap channel open"];
|
|
||||||
SEND_SABM_0->W4_UA_0 [label = "SEND SABM"];
|
|
||||||
W4_UA_0->OPEN [label = "RECV UA#0"];
|
|
||||||
CLOSED -> W4_SABM_0 [label = "l2cap channel open incoming"];
|
|
||||||
W4_SABM_0->SEND_UA_0 [label = "RECV SABM #0"];
|
|
||||||
SEND_UA_0->OPEN [label = "SEND UA#0"];
|
|
||||||
|
|
||||||
OPEN->SEND_UA_0_AND_DISC [label = "RECV DISC#0"];
|
|
||||||
SEND_UA_0_AND_DISC->CLOSED [label = "SEND UA#0"];
|
|
||||||
OPEN->CLOSED [label = "RECV DM#0"];
|
|
||||||
}
|
|
||||||
Loading…
x
Reference in New Issue
Block a user