learning:tla_summary

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
learning:tla_summary [2025/08/20 10:11] – fponzilearning:tla_summary [2025/08/20 10:20] (current) – fponzi
Line 11: Line 11:
 ^ Construct ^ Description ^ ^ Construct ^ Description ^
 | **module M** | Begins the module or submodule named //M//. | | **module M** | Begins the module or submodule named //M//. |
-| **extends M1, ..., Mn** | Incorporates declarations, definitions, assumptions, and theorems from modules //M1, ..., Mn// into the current module. | +| **extends M1, ..., Mn** | Incorporates the declarations, definitions, assumptions, and theorems from the modules named //M1, ..., Mn// into the current module. | 
-| **constants C1, ..., Cn** | Declares constants (rigid variables). Each Cj may be an identifier or an operator with arguments. | +| **constants C1, ..., Cn** | Declares the Cj to be constant parameters (rigid variables). Each Cj is either an identifier or has the form C(-,...,-), the latter form indicating that C is an operator with the indicated number of arguments. | 
-| **variables x1, ..., xn** | Declares flexible variables. | +| **variables x1, ..., xn** | Declares the xj to be variables (parameters that are flexible variables). | 
-| **assume P** | States assumption //P//. | +| **assume P** | Asserts P as an assumption. | 
-| **F(x1, ..., xn) == exp** | Defines operator //F//. | +| **F(x1, ..., xn) == exp** | Defines F to be the operator such that F(e1,...,en) equals exp with each identifier xk replaced by ek. (For n = 0, it is written F == exp.) | 
-| **f[x ∈ S] == exp** | Defines function //f// with domain //S//. | +| **f[x ∈ S] == exp** | Defines f to be the function with domain S such that f[x] = exp for all x in S. (The symbol f may occur in exp, allowing a recursive definition.) | 
-| **instance M with p1 <- e1, ..., pm <- em** | Instantiates module //M// with substitutions. | +| **instance M with p1 <- e1, ..., pm <- em** | For each defined operator F of module M, this defines F to be the operator whose definition is obtained from the definition of F in M by replacing each declared constant or variable pj of M with ej. (If m = 0, the 'with' is omitted.) | 
-| **N(x1, ..., xn) == instance M with ...** | Parameterized instantiation of //M//. | +| **N(x1, ..., xn) == instance M with p1 <- e1, ..., pm <- em** | For each defined operator F of module M, this defines N(d1,...,dn)!F to be the operator whose definition is obtained from the definition of F by replacing each declared constant or variable pj of M with ej, and then replacing each identifier xk with dk. (If m = 0, the 'with' is omitted.) | 
-| **theorem P** | Asserts that //P// can be proved. | +| **theorem P** | Asserts that P can be proved from the definitions and assumptions of the current module. | 
-| **local def** | Makes definitions local. |+| **local def** | Makes the definition(s) of def (which may be a definition or an instance statement) local to the current module, thereby not obtained when extending or instantiating the module. |
 | **====** | Ends the current module or submodule. | | **====** | Ends the current module or submodule. |
  
Line 39: Line 39:
  
 ^ Construct ^ Description ^ ^ Construct ^ Description ^
-| **IF p THEN e1 ELSE e2** | Conditional expression. | +| **IF p THEN e1 ELSE e2** | Conditional expression: e1 if p is true, else e2. | 
-| **CASE p1 -> e1 [] ... [] pn -> en** | Pattern-based conditional. | +| **CASE p1 -> e1 [] ... [] pn -> en** | Some ei such that pi is true. | 
-| **CASE ... [] OTHER -> e** | Default case. | +| **CASE ... [] OTHER -> e** | Some ei such that pi is true, or e if all pi are false. | 
-| **LET ... IN e** | Local definitions. | +| **LET d1 == e1 ... dn == en IN e** | e in the context of the definitions. | 
-| **/\\ p1 ... pn** | Conjunction. | +| **/\\ p1 ... pn** | Conjunction p1 /\\ ... /\\ pn. | 
-| **\\/ p1 ... pn** | Disjunction. |+| **\\/ p1 ... pn** | Disjunction p1 \\/ ... \\/ pn. |
  
 ---- ----
Line 51: Line 51:
  
 ^ Operator ^ Description ^ ^ Operator ^ Description ^
-| **e'** | Value of e in next state. | +| **e'** | The value of e in the final state of a step. | 
-| **[A]_e** | A or (e' = e). | +| **[A]_e** | A ∨ (e' = e). | 
-| **<A>_e** | A and (e' ≠ e). | +| **<A>_e** | A ∧ (e' ≠ e). | 
-| **ENABLED A** | Action A is possible. |+| **ENABLED A** | An A step is possible. |
 | **UNCHANGED e** | e' = e. | | **UNCHANGED e** | e' = e. |
 | **A · B** | Composition of actions. | | **A · B** | Composition of actions. |
Line 63: Line 63:
  
 ^ Operator ^ Meaning ^ ^ Operator ^ Meaning ^
-| **[]F** | Always F. | +| **[]F** | F is always true. | 
-| **<>F** | Eventually F. | +| **<>F** | F is eventually true. | 
-| **WF_e(A)** | Weak fairness. | +| **WF_e(A)** | Weak fairness for action A. | 
-| **SF_e(A)** | Strong fairness. |+| **SF_e(A)** | Strong fairness for action A. |
 | **F ~> G** | F leads to G. | | **F ~> G** | F leads to G. |
  
Line 108: Line 108:
  
 ---- ----
 +
  • learning/tla_summary.txt
  • Last modified: 2025/08/20 10:20
  • by fponzi