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

Re: [tlaplus] Novel queue-lock like concurrent spin-lock formalization in TLA+

On 22.03.21 09:50, Dan Tisdall wrote:
For now my idea has been to use a VIEW to hide the history, use a counter to fix the total number of operations, and then make exactly one process print the history at the end of the 'program' (after n operations have been performed). I won't then check this history in-model but rather just use the printed result in an external tool.

If you have to check the results in an external tool, the Json module [1] might help.


[1] https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c8ab61ee-ccdc-1044-682d-102dfa19c628%40lemmster.de.