+NAME("irc"). +VSN("ubf1.0"). +TYPES info() = info; description() = description; contract() = contract; ok() = ok; bool() = true | false; nick() = string(); oldnick() = nick(); newnick() = nick(); group() = string(); groups() = [group()]; logon() = logon; proceed() = {ok, nick()}; listGroups() = groups; joinGroup() = {join, group()}; leaveGroup() = {leave, group()}; changeNick() = {nick, nick()}; msg() = {msg, group(), string()}; msgEvent() = {msg, nick(), group(), string()}; joinEvent() = {joins, nick(), group()}; leaveEvent() = {leaves, nick(), group()}; changeNameEvent() = {changesName, oldnick(), newnick(), group()}. +STATE start logon() => proceed() & active. %% Nick randomly assigned +STATE active listGroups() => groups() & active; joinGroup() => ok() & active; leaveGroup() => ok() & active; changeNick() => bool() & active; msg() => bool() & active; %% False if you have not joined a group EVENT => msgEvent(); %% Group sends me a message EVENT => joinEvent(); %% Nick joins group EVENT => leaveEvent(); %% Nick leaves group EVENT => changeNameEvent(). %% Nick changes name +ANYSTATE info() => string(); description() => string(); contract() => term().