logic ExtModal
spec Try1=
time modality t
modalities a,b
nominals N, M
end