[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.