流水

TLA+语言

2019/12/10 TLA+

TLA+语言语法

TLA+语言

[TOC]

TLA+描述语言

有两种语法：TLA+语言， plusCal语言. plusCal的描述能力不如TLA+强大，但plusCal更接近编程模式。 plusCal要转换成TLA+之后才能用TLC检查。

PlusCal is an algorithm language. An algorithm language is meant for writing algorithms, not programs. Algorithms differ from programs in several ways:

  • 算法的操作对象可以是任意数学对象，program只能操作简单对象 Algorithms perform operations on arbitrary mathematical objects,such as graphs and vector spaces. Programs perform operations on simple objects such as Booleans and integers; operations on more complex data types must be coded using lower-level operations such as integer addition and method invocation.
  • program描述计算一个结果的方法，algorithm描述一类计算（聚焦？） A program describes one method of computing a result; an algorithm may describe a class of possible computations. For example, an algorithm might simply require that a certain operation be performed for all values of i from 1 to N . A program specifies in which order those operations are performed.
  • algorithm的执行由一个step的序列组成，复杂度在step的数量上。 Execution of an algorithm consists of a sequence of steps. An algorithm’s computational complexity is the number of steps it takes to compute the result; defining a concurrent algorithm requires specifying what constitutes a single (atomic) step. There is no well-defined notion of a step of a program.

整体项目组织

spec 下有module和model。 module为源码，model用来配置TLC测试他们

源文件格式
---- MODULE module_name ----          《---module_name为代码源文件名。  ---- MODULE和====之间的才是代码，其他都忽略，TLC不会分析。
EXTENDS Naturals, TLC                          《--类似其他语言的#include 或import，导入其他module

\*此处放tla+语言代码

(*  --algorithm algorithm_name               《--    --algorithm用于告诉pluscal转换器这是pluscal语言的代码。每个文件只能有一个。name随便起
	\*放pluscal语言代码（pascal或c风格）        《--pluscal代码时放在注释块中的，即(* *)
*)

\* BEGIN TRANSLATION
此处会放pluscal转换后的tla+语言代码
\* END TRANSLATION

\*此处放tla+语言代码

====
pluscal语言格式
pascal风格：
(* --algorithm algorithm_name
variables x = 1, y \in {3, 4}, z = {3, 4};
begin
	\* PlusCal code
end algorithm; 
*)
c风格
(* --algorithm transfer 

{
    variables alice_account = 10, bob_account = 10,
        account_total = alice_account + bob_account;

    process(transaction \in 1..2)
        variable money \in 1..20;               《---在process的情况下，money同一时刻就是两个value了，对每个process一个
    { 
    start: 
        if (alice_account >= money) 
        { 
            alice_account := alice_account - money;
            bob_account := bob_account + money;
        };
        print alice_account;
        
    over: 
        assert alice_account >= 0;
    }
}

*)

reserved words

The PlusCal reserved words are：

assert await begin call define do either else elsif end goto if macro or print procedure process return skip then variable variables when while with

A TLA+ identifier is a record-component that is not one of the following： TLA+的保留字

ASSUME ASSUMPTION AXIOM CASE CHOOSE CONSTANT CONSTANTS DOMAIN ELSE ENABLED EXCEPT EXTENDS IF IN INSTANCE LET LOCAL MODULE OTHER UNION SUBSET THEN THEOREM UNCHANGED VARIABLE VARIABLES WITH

Search

    Table of Contents