[tlaplus] Fairness in programming languages

[Jones Martins <jonesmvc@xxxxxxxxx>]

Hello everyone,

Maybe I'm asking the wrong question or thinking in the wrong way.

When specifying a system in TLA⁺, it's useful to describe if certain actions are strongly fair, weakly fair or not fair at all, so that we can verify temporal properties with TLC. When implementing such a system with a programming language, how would we go about implementing these fairness requirements? Is fairness something our implementation does by itself, so we don't need to mention it at all? Is fairness defined in the kernel? Etc.

Best regards,

Jones Martins

-- 
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/fb01eabf-d7ff-40a1-9187-10232a9231bdn%40googlegroups.com.