Skip to content

Commit

Permalink
Fix typo in the tla rule comments (#462)
Browse files Browse the repository at this point in the history
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
marshtompsxd authored Mar 22, 2024
1 parent 4d12d81 commit c2cfdf9
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/temporal_logic/rules.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1352,7 +1352,7 @@ pub proof fn strengthen_next<T>(spec: TempPred<T>, next: ActionPred<T>, inv: Sta

/// Get the initial leads_to.
/// pre:
/// spec |= [](p /\ next => p' /\ q')
/// spec |= [](p /\ next => p' \/ q')
/// spec |= [](p /\ next /\ forward => q')
/// spec |= []next
/// spec |= []p ~> forward
Expand Down Expand Up @@ -1421,7 +1421,7 @@ pub proof fn wf1_variant_borrow_from_spec_temp<T>(spec: TempPred<T>, next: TempP

/// Get the initial leads_to with a stronger wf assumption than wf1_variant.
/// pre:
/// |= p /\ next => p' /\ q'
/// |= p /\ next => p' \/ q'
/// |= p /\ next /\ forward => q'
/// |= p => enabled(forward)
/// spec |= []next
Expand Down

0 comments on commit c2cfdf9

Please sign in to comment.