Skip to content

Commit

Permalink
Fix tla-example-with-functor.dl to use list fold functor.
Browse files Browse the repository at this point in the history
  • Loading branch information
Anastasios Antoniadis committed Jan 12, 2025
1 parent bbc6f40 commit 397def1
Showing 1 changed file with 4 additions and 14 deletions.
18 changes: 4 additions & 14 deletions tla-example-with-functor.dl
Original file line number Diff line number Diff line change
Expand Up @@ -97,24 +97,14 @@ ClientServerIndex(c, s, ci*ns + si) :-
serverId : ServerId
]

// .type LockedState = [
// serverIndex: number,
// rest: LockedState
// ]

// .type HeldState = [
// clientServerIndex: number,
// rest: HeldState
// ]

.type HeldOrLockedState = [
index: number,
rest: HeldOrLockedState
]

.type State = [
locked: LockedState,
held: HeldState
locked: HeldOrLockedState,
held: HeldOrLockedState
]


Expand Down Expand Up @@ -168,12 +158,12 @@ DecomposeAction(a, k, c, s) :-
.decl HeldStateFinalized(prevState: State, action: Action, hstate: HeldOrLockedState)
HeldStateFinalized(prevState, action, id_list) :-
PossibleAction(prevState, action),
id = @@list_fold i: 0, {Held_Prime_Index(prevState, action, i)}.
id_list = @@list_fold i: nil, {Held_Prime_Index(prevState, action, i)}.

.decl LockedStateFinalized(prevState: State, action: Action, lstate: HeldOrLockedState)
LockedStateFinalized(prevState, action, id_list) :-
PossibleAction(prevState, action),
id = @@list_fold i: 0, {Locked_Prime_Index(prevState, action, i)}.
id_list = @@list_fold i: nil, {Locked_Prime_Index(prevState, action, i)}.

.decl TotalStateFinalized(state: State, prevState: State, action: Action)
TotalStateFinalized([ls, hs], prevState, action) :-
Expand Down

0 comments on commit 397def1

Please sign in to comment.