How does porcupine handle timeouts?

[symbiont-sean-lyons]

How can one represent the ambiguity of timeout responses with porcupine?

When my application fails to handle a request by some specified deadline, it is unclear whether the request took effect or not. Knossos handles this ambiguity with the :info response type, but porcupine doesn't seem to have an equivalent. I think this concern needs to be built into the checker.

So how can porcupine handle ambiguous histories created by phenomena like timeouts?

[anishathalye]

I think you can do this without modifying Porcupine code. You can model timed out calls by having them "return" at time infinity (in practice, any large number that's greater than all the non-failed calls' return times). And you can incorporate a notion of these failed requests into your sequential specification by computing the state update as you would do normally but skipping the return value check for them.

Let me know if this succinct sketch makes sense, otherwise I can elaborate.

[anishathalye]

Closing due to inactivity; feel free to reopen if you still have a question.