I wrote this code, what is wrong?
-------------------------------- MODULE POW --------------------------------
EXTENDS Integers
CONSTANT nodes
VARIABLES chain, blcks, last_block_id, status, status_changer
Block == [miner_id: nodes \union {"first"}, block_id: 0..3, prev_block_id: -1..3]
POWTypeOK ==
/\ blcks \subseteq Block
/\ chain \in [nodes -> SUBSET Block]
/\ last_block_id \in [nodes -> 0..3]
/\ status \in [nodes -> {"mined", "miner"}]
/\ status_changer \in [nodes -> {0, 1}]
----------------------------------------------------------------------------
POWInit ==
/\ blcks = {[miner_id |-> "first", block_id |-> 0, prev_block_id |-> -1]}
/\ chain = [n \in nodes |-> {[miner_id |-> "first", block_id |-> 0, prev_block_id |-> -1]}]
/\ last_block_id = [n \in nodes |-> 0]
/\ status = [ n \in nodes |-> "miner"]
/\ status_changer = [n \in nodes |-> 0]
----------------------------------------------------------------------------
MineABlock(n) ==
/\ status[n] = "miner"
/\ chain' = [chain EXCEPT ![n] = chain[n] \union {[miner_id |-> n, block_id |-> last_block_id[n] + 1,
prev_block_id |-> last_block_id[n]]}]
/\ blcks' = blcks \union {[miner_id |-> n, block_id |-> last_block_id[n] + 1, prev_block_id |-> last_block_id[n]]}
/\ last_block_id' = [last_block_id EXCEPT ![n] = last_block_id[n] + 1]
/\ status' = [status EXCEPT ![n] = "mined"]
/\ status_changer' = [status_changer EXCEPT ![n] = 1]
CommitABlock(n, r) ==
/\ status[n] = "mined"
/\ last_block_id[r] = last_block_id[n] - 1
/\ [miner_id |-> n, block_id |-> last_block_id[n], prev_block_id |-> last_block_id[n] - 1] \in blcks
/\ chain' = chain
/\ chain[r]' = chain[r] \union {[miner_id |-> n, block_id |-> last_block_id[n], prev_block_id |-> last_block_id[r]]}
/\ last_block_id' = [last_block_id EXCEPT ![r] = last_block_id[n]]
/\ status_changer' = [status_changer EXCEPT ![r] = 1]
/\ UNCHANGED <<blcks, status>>
IgnoreABlock(n, r) ==
/\ status[n] = "mined"
/\ [miner_id |-> n, block_id |-> last_block_id[n], prev_block_id |-> last_block_id[n] - 1] \in blcks
/\ status_changer' = [status_changer EXCEPT ![r] = 1]
/\ UNCHANGED <<chain, blcks, last_block_id, status>>
ChangeStatus(n) ==
/\ status_changer = [r \in nodes |-> 1]
/\ status' = [status EXCEPT ![n] = "miner"]
/\ status_changer' = [r \in nodes |-> 0]
/\ UNCHANGED <<blcks, chain, last_block_id>>
-----------------------------------------------------------------------------
POWNext == (\E n\in nodes:
\/ MineABlock(n) \/ ChangeStatus(n)
\/ (\A r \in nodes: CommitABlock(n, r) \/ IgnoreABlock(n, r)))
-----------------------------------------------------------------------------
POWSpec == POWInit /\ [][POWNext]_<<chain, blcks, last_block_id, status>>
(*************************************************************************)
(* The complete spec of the Proof-of-work Commit protocol. *)
(*************************************************************************)
THEOREM POWSpec => []POWTypeOK
(*************************************************************************)
(* This theorem asserts that the type-correctness predicate POWTypeOK is *)
(* an invariant of the specification. *)
(*************************************************************************)
--
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/b55367fa-bc1e-4d5a-8150-6bc146fa90e2n%40googlegroups.com.