分布式事务有自己的架构语言吗？TLA +简介

TLA +是一种正式的规范语言。它是设计系统和算法的工具，然后以编程方式验证这些系统没有严重错误。它是相当于蓝图的软件。通常用于设计分布式事务系统，亚马逊等公司普遍使用该语言规范设计他们的分布式事务中间件基础设施。是分布式架构设计语言。

我为什么要用它？
这是一个简单的TLA +规范，代表人们交易独特的项目。你能找到这个bug吗？

People == {"alice", "bob"}
Items == {"ore", "sheep", "brick"}
(* --algorithm trade
variable owner_of \in [Items -> People]

process giveitem \in 1..3 \* up to three possible trades made
variables item \in Items, 
          owner = owner_of[item], 
          to \in People,
          origin_of_trade \in People
begin Give:
    if origin_of_trade = owner then 
        owner_of[item] := to;
    end if;
end process;
end algorithm; *)

这是一个交易案例，为了防止金融诈骗，我们应该检查Item条目的所有者是否是交易者？但是如果我们运行模型检查器，我们发现这段代码不能完成我们的目标：Alice可以与自己进行项目交易，并且在该过程完成运行之前，通过并行交易，将相同项目交给Bob。然后第一笔交易结算完成，Alice收回项目。我们的算法在竞争条件下失败，我们通过TLA+知道了这一点，因为TLA +探索了每个可能的状态和时间线。

有几种不同的方法来解决这个问题。但我们的解决方案是否适用于两个以上的人？在TLA +中，检查就如同People == {"alice", "bob", "eve"}一样简单；如果我们可以一次交易多个项目，它会起作用吗？variable items \in SUBSET Items；如果有多只绵羊，矿石和砖块怎么办？amount_owned = [People \X Items -> 0..5；。如果三个人与其他每个玩家交易1个矿石和1个羊，而Eve和Alice交易 0砖那会怎么样？如果它处于可能的状态空间，TLA +将检查它。

难以使用吗？
形式方法因其难以达到关键系统的价值而闻名。这意味着所有指南都是在读者正在研究关键系统的情况下编写的，他们必须在内部和外部了解TLA +以确保他们的系统不会意外杀死人。
如果对你来说一个危险的错误是“有人死了”，那么是的，形式方法很难。如果一个危险的错误是“没有人死，但我们的客户真的很生气，我们不得不花两周的时间追踪并修复错误”，那么你需要的小部分TLA +实际上很容易学习。只需找到一个适合初学者的指南，你就可以了。

哪里是初学者友好指南？
你好！本指南以简单实用的方式介绍了TLA +的基础知识。如果您想从头开始，您可以了解我们将在此处介绍的内容。