Re: Mixing TLA+ and SOS

Hi Behrooz,

obviously yes you can. A semantic is specified with a series of functions F: E X. S --> S or inference rules

where E are expressions and S is a state (variables with their values). Here you specify your expressions

thanks to records in a treeish way (this avoids the need to parse your expressions). And your state by TLAPLUS

variables. And the functions by functions and inference rules by TLAPLUS actions.