Skip to content

run_parallel_commands doesn't handle postcondition result the same way run_commands does #72

yrashk opened this Issue Aug 5, 2013 · 1 comment

2 participants

yrashk commented Aug 5, 2013

run_commands handles exceptions by wrapping them into a postcondition result, while run_parallel_commands (through check/6) only checks for true and false.


run_parallel_commands should be used for parallel execution, assuming that (at least sequentially) no exceptions are raised. You suggest that check/6 should not only check whether a post-condition is true or false. It should additionally catch exceptions raised from Mod:postcondition(State, Call, Res) and handle such cases the same way as false postconditions, i.e. possibly leading to a non_possible_interleaving result. Is this correct?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.