多进程之前使用的例子都是单进程的，现在用多进程来描述多个逻辑同时发生，TLA+中的多进程可以理解为其他高级语言中的多线程。为了方便理解，使用Pluscal语言来描述，TLA+ Toolbox可以将pluscal语言转化为TLA+，基本格式如下：---- MODULE module_name ----\* TLA+ code(* --algorithm algorithm_name\* 固定格式，a

数字人民币的可编程性与智能合约农行深圳分行与华为在深圳联合举办数字人民币智能合约成果发布会上联合发布了租赁资金监管领域的创新应用成果，标志着业内基于数字人民币的首个云侧智能合约应用成果落地。该方案中，智能合约由租赁双方约定数字人民币的交付规则并自动支付（如房租支付和押金退回），让数字人民币在使用方面具有便捷性和多样性。这里面涉及到数字人民币与智能合约，先看下两者的定义：数字人民币定义以下是数字人民