fmod CONF is

protecting NAT .
protecting PROC .

var procset : ProcSet .

sort Conf .

var conf : Conf .

op regconf : ProcSet Nat -> Conf .
op transconf : ProcSet Nat Conf -> Conf .  --- contains prev reg conf

var index : Nat .

op members : Conf -> ProcSet .
eq members(regconf(procset,index)) = procset .
eq members(transconf(procset,index,conf)) = procset .

op index : Conf -> Nat .
eq index(regconf(procset,index)) = index .
eq index(transconf(procset,index,conf)) = index .

op reg : Conf -> Conf .
eq reg(regconf(procset,index)) = regconf(procset,index) .
eq reg(transconf(procset,index,conf)) = conf .


endfm