Skip to content

Commit

Permalink
Rename function
Browse files Browse the repository at this point in the history
  • Loading branch information
thpani committed Apr 30, 2024
1 parent 94ba9ea commit 9448d16
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions solarkraft/src/verify.ts
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ export function instrumentMonitor(
state.push({ name: 'last_error', type: 'TlaStr', value: '' })

// Declaration of "Init" (according to `state`)
const tlaInit = tlaJsonOperDecl__Conjunction(
const tlaInit = tlaJsonOperDecl__And(
'Init',
state.map((binding) =>
tlaJsonEq__NameEx__ValEx(
Expand All @@ -54,7 +54,7 @@ export function instrumentMonitor(
{ name: 'timestamp', kind: 'TlaInt', value: tx.env.timestamp },
])
const txArgs = tx.functionArgs.map((v) => tlaJsonValEx(v.type, v.value))
const tlaNext = tlaJsonOperDecl__Conjunction('Next', [
const tlaNext = tlaJsonOperDecl__And('Next', [
tlaJsonApplication(tx.functionName, [envRecord].concat(txArgs)),
tlaJsonEq__NameEx__ValEx(
'last_error',
Expand All @@ -81,7 +81,7 @@ export function instrumentMonitor(
* @param conjuncts Body conjuncts
* @returns The operator declaration in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html
*/
function tlaJsonOperDecl__Conjunction(
function tlaJsonOperDecl__And(
operDeclName: string,
conjuncts: any
): any {
Expand Down

0 comments on commit 9448d16

Please sign in to comment.