%%%%  Productive system example: traffic lights  %%%%
%% traffic light: single light, no timer
% color : type.
% red : color.
% yellow : color.
% green : color.
% 
% light : color -> type.
% 
% change1 : light red -o {light green}.
% change2 : light green -o {light yellow}.
% change3 : light yellow -o {light red}.
% 
% #trace * {light green}.

% traffic light: single light, timer
% color : type.
% red : color.
% yellow : color.
% green : color.
% 
% nat : type.
% z : nat.
% s : nat -> nat.
% 
% n1 : nat = s z.
% n2 : nat = s n1.
% n3 : nat = s n2.
% n4 : nat = s n3.
% n5 : nat = s n4.
% 
% light : color -> type.
% timer : nat -> type.
% 
% change1 : timer z * light red -o {light green * timer n4}.
% change2 : timer z * light green -o {light yellow * timer n1}.
% change3 : timer z * light yellow -o {light red * timer n3}.
% 
% tick : timer (s N) -o {timer N}.
% 
% #trace * {timer z * light green}.

% traffic light: multiple timed lights; unsynchronized; badness
% color : type.
% red : color.
% yellow : color.
% green : color.
% 
% next : color -> color -> type.
% - : next red green.
% - : next green yellow.
% - : next yellow red.
% 
% nat : type.
% z : nat.
% s : nat -> nat.
% 
% plus : nat -> nat -> nat -> type.
% plus/z : plus z N N.
% plus/s : plus (s N) M (s P)
%           <- plus N M P.
% 
% n1 : nat = s z.
% n2 : nat = s n1.
% n3 : nat = s n2.
% n4 : nat = s n3.
% n5 : nat = s n4.
% 
% dir : type.
% ns : dir.
% ew : dir.
% 
% duration : dir -> color -> nat -> type.
% - : duration ns red n3.
% - : duration ns green n4.
% - : duration ns yellow n1.
% 
% - : duration ew red (s X)
%      <- duration ns green G
%      <- duration ns yellow Y
%      <- plus G Y X.
% 
% - : duration ew yellow n1.
% 
% - : duration ew green X
%      <- duration ns red (s X).
% 
% light : dir -> color -> type.
% timer : dir -> nat -> type.
% 
% change : timer D z 
%        * light D C 
%        * next C C' 
%        * duration D C' T
%              -o {light D C' * timer D T}.
% 
% tick : timer D (s N) -o {timer D N}.
% 
% crash_OH_NO : type.
% oops : light D green * light D' green * timer X Y * timer Z W -o 
%            {crash_OH_NO}.
% 
% init : type = 
%   {timer ns z * light ns green * timer ew z * light ew red}.
% 
% 
% #trace * init.
% #query * * * 1 init -o {crash_OH_NO}. 


%% traffic lights: synchronized changing
% color : type.
% red : color.
% yellow : color.
% green : color.
% 
% nat : type.
% z : nat.
% s : nat -> nat.
% 
% plus : nat -> nat -> nat -> type.
% plus/z : plus z N N.
% plus/s : plus (s N) M (s P)
%           <- plus N M P.
% 
% n1 : nat = s z.
% n2 : nat = s n1.
% n3 : nat = s n2.
% n4 : nat = s n3.
% n5 : nat = s n4.
% 
% 
% duration : color -> nat -> type.
% - : duration red n3.
% - : duration green n4.
% - : duration yellow n1.
% 
% timer : nat -> type.
% 
% dir : type.
% ns : dir.
% ew : dir.
% light : dir -> color -> type.
% 
% change1 : timer z 
%         * light ns yellow 
%         * light ew red
%         * duration red T
%           -o {light ns red * light ew green * timer T}.
% 
% change2 : timer z
%         * light D green
%         * duration yellow T
%           -o {light D yellow * timer T}.
% 
% change3 : timer z
%         * light ns red
%         * light ew yellow
%         * duration green T
%           -o {light ns green * light ew red * timer T}.
% 
% tick : timer (s N) -o {timer N}.
% 
% crash_OH_NO : type.
% oops : light D green * light D' green * timer T -o 
%            {crash_OH_NO}.
% 
% init : type = 
%   {timer z * light ns green * light ew red}.
% 
% #trace * init.
% % #query * * * 1 init -o {crash_OH_NO}.