Lamport on Temporal Logic of Actions and refinement mapping

Leslie Lamport, winner of the Association for Computing Machinery's A.M. Turing Award, discuses his Temporal Logic of Actions (TLA) language for modeling and verifying distributed algorithms and systems. He also explains its connection to his work on refinement mapping. This clip is taken from an interview conducted with Lamport by Roy Levin for the ACM and Computer History Museum on August 12, 2016 in Mountain View, CA. Video of the full interview is available as part of Lamport’s ACM profile at amturing.acm.org/award_winner....

[@stoyanfurdzhev]

Is action actually a matemática operation aplayed to s quantitative rapresentation obtained by a series of operations aplayed to the number one?