[SAL-HELP] Union type and sub-program in SAL?

[Xi L.]

Hi,

I am using SAL to model check our complex transition system semantics
against linear temporal formula. Sorry to have asked these silly
questions.

Now I am wondering is it possible to define a union type in SAL. Like
variable x can be of type int or some complex type e.g. a set. If not,
could you please tell me how to implement union in SAL?

Besides, is function -- sub-program available in SAL? Then if two
transitions may take similar steps, but complex, I do not need to
write it twice.

Best wishes,

-- 
Sincerely,

William