libmctp serial binding mctp_write_all() specification

write_all.tla

----------------------------- MODULE write_all -----------------------------
EXTENDS Integers, TLC, Sequences

CONSTANT L
VARIABLE wrote, remaining, result

vars == << wrote, remaining, result >>
    
write_errors == { -11, -9, -89, -122, -14, -27, -4, -22, -5, -28, -1, -32 }

Safety ==
    /\ remaining >= 0
    /\ remaining <= L
    /\ \/ /\ wrote = 0
          /\ remaining = L
       \/ /\ wrote > 0
          /\ wrote <= remaining
       \/ /\ wrote \in write_errors
          /\ remaining > 0
    
Liveness == <>(result \in (write_errors \union {0}))

mctp_write_fn(len) ==
    LET results == write_errors \union 1..len
    IN CHOOSE r \in results: r <= len

Init ==
    /\ remaining = L
    /\ wrote = 0
    /\ result = 0

mctp_write_success ==
    /\ remaining > 0
    /\ ~(wrote \in write_errors)
    /\ wrote' = mctp_write_fn(remaining)
    /\ remaining' = remaining - wrote
    /\ result' = IF (remaining - wrote) = 0 THEN 0 ELSE wrote
    
mctp_write_failure ==
    /\ remaining > 0
    /\ wrote \in write_errors
    /\ wrote' = wrote
    /\ remaining' = remaining
    /\ result' = wrote
    
mctp_write_all == mctp_write_success \/ mctp_write_failure

Next == mctp_write_all \/ UNCHANGED vars
         
Spec == Init /\ [][Next]_vars /\ WF_vars(mctp_write_all)

=============================================================================
\* Modification History
\* Last modified Tue Oct 04 23:09:31 ACDT 2022 by andrew
\* Created Tue Oct 04 10:25:39 ACDT 2022 by andrew