GenAutomata Sections NuprlLIB Doc

Def (M |= x,x',tr,tr'.R(x;x';tr;tr')) == x,x':M.state, tr:M.action List, a:M.action. (M -tr- > x) M.trans(x,a,x') R(x;x';tr;tr @ [a])

is mentioned

In prior sections: mb state machine


GenAutomata Sections NuprlLIB Doc