CoreDump: PML to TLA+: An Example.
Jan 8, 2022
Welcome to CoreDUmp, the one stop for techies, in this episode the Trio, return from Redmond, armed with TLA+ tools!
Gecko: Dr Bheemaiah has invented PML, I can show you an example from PML to TLA+, Let me pick this example. It is from Car Talk!
Here is the PML:
A single class Solution,
With the TLA+ code defined, from the link above,
Trio: This is cool, we can write an automated code generator from PML to TLA+, with classes and relationships converted to straight TLA+ with the required scoping! and feed this to Zenon! Great UML or PML for Alloy or TLA+
Gecko: Great model driven provable programming!
Trio: We are off to provable M.L now….
