TLA+ model (in PlusCal) demonstrating race condition & resolving it

model_with_race_condition.tla

EXTENDS Naturals, TLC

(* --algorithm transfer
variables db_data = {}, read_db_data = {}, published_rx_data = {}, new_entry = 1, subscribed = FALSE;

fair process writer = "writer"
variables local_db_data = {}
begin
  WRITER_OPEN: local_db_data := db_data; \* open transaction
  WRITER_WRITE: local_db_data := local_db_data \union {new_entry}; \* write
  WRITER_COMMIT: db_data := db_data \union local_db_data; \* commit
  WRITER_PUBLISH: if subscribed = TRUE then
                    published_rx_data := published_rx_data \union {new_entry}; \* publish to observable
                  end if;
end process
  
fair process reader = "reader"
variables local_db_data = {}
begin
  READER_OPEN: local_db_data := db_data; \* open transaction
  READER_READ: read_db_data := local_db_data; \* read
  READER_SUBSCRIBE: subscribed := TRUE; \* subscribe
  \* READER_COMMIT doing nothing on read
end process

end algorithm *)

\* BEGIN TRANSLATION
...
\* END TRANSLATION

\* The condition to be added as a temporal property in the model
VisibleData == <>(new_entry \in read_db_data \/ new_entry \in published_rx_data)

model_without_race_condition.tla

EXTENDS Naturals, TLC

(* --algorithm transfer
variables db_data = {}, read_db_data = {}, published_rx_data = {}, new_entry = 1, subscribed = FALSE;

fair process writer = "writer"
variables local_db_data = {}
begin
  WRITER_OPEN: local_db_data := db_data; \* open transaction
  WRITER_WRITE: local_db_data := local_db_data \union {new_entry}; \* write
  WRITER_COMMIT: db_data := db_data \union local_db_data; \* commit
  WRITER_PUBLISH: if subscribed = TRUE then
                    published_rx_data := published_rx_data \union {new_entry}; \* publish to observable
                  end if;
end process
  
fair process reader = "reader"
variables local_db_data = {}
begin
  READER_SUBSCRIBE: subscribed := TRUE; \* subscribe
  READER_OPEN: local_db_data := db_data; \* open transaction
  READER_READ: read_db_data := local_db_data; \* read
  \* READER_COMMIT doing nothing on read
end process

end algorithm *)

\* BEGIN TRANSLATION
...
\* END TRANSLATION


\* The condition to be added as a temporal property in the model
VisibleData == <>(new_entry \in read_db_data \/ new_entry \in published_rx_data)