Finding identities for the Noki 5110

Harold Thimbleby - http://www.uclic.ucl.ac.uk/harold

This file is the background for establishing some matrix identities for the Nokia 5110 example used in the papers.

Define the Nokia 5110 FSM

First we define the Nokia using a tree, and symbolic names taken from the device itself. This tree was then carefully checked against the Nokia itself.

\(\(readable[nokia] ^= 
        menu["standby", {menu["phone book", {"search", "service nos", "add entry", "erase", "edit", "send entry", 
                menu["options", {"type of view", "memory status"}], "speed dials"}], 
            menu["messages", {"inbox", "outbox", "write messages", 
                menu["message settings", {menu["set 1", {"message centre number", "messages sent as", "message validity"}], 
                    menu["common", {"delivery reports", "reply via same centre"}]}], "info service", "voice mailbox number"}], 
            menu["call register", {"missed calls", "received calls", "dialled numbers", "erase recent calls", 
                menu["show call duration", {"last call duration", "all calls' duration", "received calls' duration", "dialled calls' duration", "clear timers"}], 
                menu["show call costs", {"last call cost", "all calls' cost", "clear counters"}], 
                menu["call costs settings", {"call costs' limit", "show costs in"}]}], 
            menu["settings", {menu["call settings", {"automatic redial", "speed dialling", "call waiting options", "own number sending", "automatic answer"}], 
                menu["phone settings", 
{menu["language", {"Automatic", "Engish", "Deutsch", "Français", "Nederlands", "Italiano", "Dansk", "Svenska", "Norsk", "Suomi", "Español", "Português", "<Russian>", "Eesti", "Latviesu", "Lietuviu", "<Arabic>", "<Hebrew>"}], "cell info display", "welcome note", "network selection", "lights"}], 
                menu["security settings", {"PIN code request", "fixed dialling", "closed user group", "phone security", "change access codes"}], "restore factory settings"}], 
            
            menu["call divert", {"divert all calls without ringing", "divert when busy", "divert when not answered", "divert when phone off or no coverage", "cancel all diverts"}], 
            menu["games", {"memory", "snake", "logic"}], "calculator", 
            menu["clock", {"alarm clock", "clock settings"}], 
            menu["tones", {"incoming call alert", "ringing tone", "ringing volume", "message alert tone", "keypad tones", "warning and game tones", "vibrating alert"}]}];\)\)

Convert tree to matrix

menuname[menu[name_, _]] := name;

menuname[name_] := name;

ToStateNo[device_, s_List] := Map[ToStateNo[device, #] &, s]

ToStateNo[device_, tran[a_, b_, c_]] := 
      tran[ToStateNo[device, a], b, ToStateNo[device, c]]

ToStateNo[device_, 
        s_] := Position[vocabulary[device], s][[1, 
        1]]

FromStateNo[device_, n_] := Part[vocabulary[device], n]

Normalise function inserts self-transitions as needed.

normalise[bm_] := 
      Module[{m = bm}, 
  
Do[
          If[Plus @@ m[[i]] == 0, 
            m[[i, i]] = 1], {i,  
            Length[m]}]; 
Return[
          m]
]

initialise[device_, 
          fullName_] := 
Module[{p, b, 
            bm}, 
vocabulary[device] ^= 
            Union@Flatten[
                symbolicTransitions[device] /. 
                  tran[a_, _, b_] -> {a, b}]; 
          numericTransitions[device] ^= 
            ToStateNo[device, symbolicTransitions[device]]; 
          numericGoals[device] ^= ToStateNo[device, #] & /@ 
              symbolicGoals[device]; 
          numberOfStates[device] ^=  
            Max@Flatten[
                numericTransitions[device] /. 
                  tran[a_, _, b_] -> {a, b}]; 
buttons[
              device] ^= 
            Union[symbolicTransitions[device] /. 
                tran[_, but_, _] -> 
                  but]; 
startStateNo[device] ^= 
            ToStateNo[device, startState[device]]; 
For[
            b = 1, b ≤ 
              Length@buttons[device], b++, 
bm = 
              Table[0, {numberOfStates[device]}, {numberOfStates[device]}]; 
            Scan[(bm[[#[[1]], #[[3]]]] = 1) &, 
Cases[
                numericTransitions[device], 
                tran[_, buttons[
                      device][[b]], _]]]; 
button[
                device, b] = 
              normalise[bm];
]; 
name[
              device] ^= fullName;
];

\(build[
        nokia] := 
Module[{auxconvert, transition, p = {}, 
          goals = {}}, 
transition[from_, button_, to_] := 
          AppendTo[p, tran[menuname[from], button, menuname[to]]]; 
        auxconvert[
            menu[name_, 
              items_]] := 
Module[{i}, 
transition[name, "Select", 
              items[[1]]]; 
For[i = 1, i ≤ Length@items, \(i++\), 
              transition[
                items[[i]], "Down", 
                items[[If[i == Length@items, 1, 
                    i + 1]]]]; 
              transition[
                items[[i]], "Up", 
                items[[If[i == 1, Length@items, 
                    i - 1]]]]; 
              transition[
                items[[i]], "C", 
                name]; 
If[
                Head@items[[i]] === 
                  menu, auxconvert[
                  items[[i]]], 
                AppendTo[goals, 
                  operation@
                    menuname[
                      items[[
                        i]]]]; 
transition[
                  items[[
                    i]], "Doit", 
                  Last@goals]; 
transition[
                  Last@goals, "Doit", 
                  items[[
                    i]]];
]
]
]; 
auxconvert[
          readable[nokia]]; 
symbolicGoals[nokia] ^= 
          goals; 
startState[
            nokia] ^= "standby"; 
symbolicTransitions[
            nokia] ^= p; 
initialise[
          nokia, "Nokia 5110 navigable menu"];
]\)

build[nokia];

Utilities for creating state vectors from state names.

vec[s_] := 
      Table[If[i == ToStateNo[nokia, s], 1, 0], {i, 
          numberOfStates[nokia]}]

devec[s_] := 
      FromStateNo[nokia, Position[s, 1][[1, 1]]]

Matrix definitions

These are the button names in the device.

buttons[nokia]

Number of states.

numberOfStates[nokia]

Define useful matrix names. The Nokia's actual Navi button is a combination of what we've called Doit and Select.

i = IdentityMatrix[numberOfStates[nokia]];

u = button[nokia, 5];
c = button[nokia, 1];
s = button[nokia, 4];
d = button[nokia, 3];
doit = button[nokia, 2];
navi = Sign[doit + s];

Find identities and interesting facts

\(Module[{i, j, k, v, 
        name}, 
v = {n, c, u, d}; 
name[
          1] = "navi"; \ name[2] = "c"; \ name[3] = "up"; \ 
      name[4] = "down"; 
For[i = 1, 
        i ≤ 4, \(i++\), 
For[j = 1, 
          j ≤ 4, \(j++\), 
For[k = 1, 
            k ≤ 4, \(k++\), 
If[
              v[\([\)\(i\)\(]\)] . v[\([\)\(j\)\(]\)] == 
                v[\([\)\(k\)\(]\)], 
Print[
                name[i], ".", name[j], "==", 
                name[k]]
]
]
]
]
]\)

Module[{zz}, 
For[zz = 0, 
        zz < 20, zz++, 
If[
          MatrixPower[c, zz] == MatrixPower[c, zz + 1], 
          Print["c^", zz, "==c^", zz + 1]; 
          Break[]]]
]

MatrixPower[c, 4] == MatrixPower[c, 5]

c . c . c . c . c == c . c . c . c

r = c . c . c . c;

r . c == r

s . s . c == s

n . d . d . d . d . d . c == n . c

r . s . s . c == r . s

r . s . c == r

r . s . s . s . c == r . s . s

rr = c . c . c; rr . s . s . c == rr . s

r . navi . navi . c == r . navi

doit . doit == i

Inverse[doit] == doit

Det[s]

u . d == i

d . u == i

u . c == c

d . c == c

doit . doit == doit

devec[vec["standby"] . s . s . c]

s . u . s . c == s . u

s . u == s . u . s . c

s . c == i

c == u . c

u . d == i

d . u == i

s . s . s . s . s == s . s . s . s . s

devec[vec["standby"] . s . u]

Module[{i, sc = s . s . c}, 
For[i = 1, 
        i ≤ 
          numberOfStates[nokia], i++, 
theState = 
          Table[If[j == i, 1, 0], {j, numberOfStates[nokia]}]; 
        If[theState . sc ≠ theState . s, 
          Print["s.s.c not identity from ", 
            devec[theState]]]
]
]