Skip to content
This repository has been archived by the owner on May 3, 2024. It is now read-only.

Commit

Permalink
Update verification/io/io-spec.gobra
Browse files Browse the repository at this point in the history
  • Loading branch information
jcp19 authored Nov 15, 2023
1 parent 6be6ae6 commit 6bf4081
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions verification/io/io-spec.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@

package io

//Unlike the original IO-spec from Isabelle, we need additional information about the network topology.
//To ensure the well-formedness of all map accesses we require an additional conjunction
//for all the events (dp.Valid())
// Unlike the original IO-spec from Isabelle, we need additional information about the network topology.
// To ensure the well-formedness of all map accesses we require an additional conjunction
// for all the events (dp.Valid())

// This is the main IO Specification.
pred (dp DataPlaneSpec) dp3s_iospec_ordered(s IO_dp3s_state_local, t Place) {
Expand Down

0 comments on commit 6bf4081

Please sign in to comment.