When generating TLA+ for a given contract, we need to use skeletons to define the builtins used by the contract. This isn't a very elegant solution and in the future we would like to have a Plutus.tla file that is generated alongside the Contract.tla file.
This is not a trivial task, however. Mainly due to the PlutusByteString datatype. For now, the multisig state machine defines a PlutusByteString as a CONSTANT and gets instantiated to a set of model values by the respective configuration files.
When generating TLA+ for a given contract, we need to use skeletons to define the builtins used by the contract. This isn't a very elegant solution and in the future we would like to have a
Plutus.tlafile that is generated alongside theContract.tlafile. This is not a trivial task, however. Mainly due to thePlutusByteStringdatatype. For now, the multisig state machine defines aPlutusByteStringas aCONSTANTand gets instantiated to a set of model values by the respective configuration files.A reasonable option could be: