PlusCal算法示例：探索TLA+规范语言

下载需积分: 50 | ZIP格式 | 381KB | 更新于2024-12-06 | 121 浏览量 | 3 下载量 举报
收藏
PlusCal 是一种算法语言，它是基于 TLA+ 算法规范系统的，由著名的计算机科学家 Leslie Lamport 所创建。TLA+ 是 Temporal Logic of Actions 的缩写，即动作时序逻辑，是一种用于描述和验证算法和系统的形式化方法。 在 TLA+ 算法规范系统中，PlusCal 是一种更接近于传统编程语言的算法描述语言。它可以用来描述复杂的算法和系统，然后使用 TLA+ 工具箱进行验证。TLA+ 工具箱提供了一套完整的验证工具，包括 TLC 算法验证检查器，它可以用来检查算法的一致性、活性和安全性等属性。 在这些示例文件中，大多数文件都是在 TLA+ 工具箱中创建的，因此它们可以在工具箱中运行，并使用 TLC 算法验证检查器进行验证。这些文件主要是支持文件，它们用于描述和验证特定的算法或系统。 在这些示例文件中，有一些文件是用于审核的重要文件，这些文件以.tla结尾，例如Euclid/Euclid.tla和HourClock/HourClock.tla。这些文件是最重要的，因为它们包含了PlusCal代码的主体部分。 PlusCal代码被包含在(*和*)的注释标记之间，从--algorithm XXX指示器开始。这表明，任何被(*和*)标记包围的代码，以及任何以--algorithm XXX开始的代码，都是PlusCal代码。 总的来说，PlusCal-Examples提供了各种PlusCal算法的示例，这些算法都是基于TLA+规范系统的。这些示例文件可以帮助我们理解如何使用PlusCal和TLA+来描述和验证复杂的算法和系统。

相关推荐

filetype

pgo：PGo是源代码，用于将PlusCal编译为Go lang

围棋 PGo是编译器将规范编译为程序的源代码。 目的/动机 是用于指定/建模并发系统的语言。 它旨在编写。 特别是，PlusCal可以编译为TLA +，可以根据有用的系统属性（使用TLC模型检查器）进行检查。 例如，是有关互斥问题的PlusCal公式解决方案的资料库。 是Google为构建分布式系统而开发的一种基于C的语言。 它内置了对通道和goroutine并发的支持，这使其非常适合开发分布式系统。 当前没有工具将PlusCal / TLA +规范与规范的实现相对应。 PGo是一种工具，旨在通过基于PlusCal规范生成Go代码来将规范与实现联系起来。 PGo可以将经过验证的分布式系统算法的PlusCal规范转换为语义上等效的Go程序。 当前状态 积极开发中。 PGo支持将大多数单进程和非常简单的多进程PlusCal算法编译为相应的可编译且可运行的Go代码。 有关最新版本的手册快照，请参见资源库中的 ，其中详细介绍了已实现的功能和几个示例。 用法 要了解如何使用PGo，请参阅。 这个怎么运作 PGo是使用Java编写的源编译器。 它将在PlusCal扩展中编写的规范（称为Mo
330 浏览量
filetype

TLA+ 术语解释及中文翻译

state 状态 A state is an assignment of values to variables. 一个状态就是一组为变量赋值的操作。 state function 状态函数 A state function is an ordinary [removed]one with no ′’′ or □\square□) that can contain variables and constants. 一个状态函数就是一个普通的表达式，包含变量和常量，但不包含 ′’′ 和 □\square□操作符. state predicate 状态谓词 A state predica
423 浏览量
filetype

tlaplus：TLC是使用TLA +编写的规范的显式状态模型检查器。 TLA +工具箱是TLA +的IDE

有关更多信息，请访问 贡献 在开始进行之前，请阅读我们的。 我们还有一个。 执照 版权所有（c）199？-2003 HP Corporation 版权所有（c）2003-2020 Microsoft Corporation 根据
218 浏览量
filetype

def adversarial(x, model, loss_func, c=1e-4, kappa=0, num_iter=100, lr=0.01): """ Create adversarial examples using CW algorithm Args: - x: input image - model: the neural network model - loss_func: the loss function to use - c: the weight for the L2 regularization term (default=1e-4) - kappa: the confidence parameter (default=0) - num_iter: number of iterations for the algorithm (default=100) - lr: learning rate for the optimization (default=0.01) Returns: - x_adv: adversarial example """ x_adv = x.clone().detach().requires_grad_(True) for i in range(num_iter): output = model(x_adv) loss = loss_func(output, torch.tensor([kappa]), x, x_adv, c) model.zero_grad() loss.backward() with torch.no_grad(): x_adv += lr * x_adv.grad x_adv = torch.max(torch.min(x_adv, x + 0.35), x - 0.35) x_adv = torch.clamp(x_adv, 0, 1) x_adv.requires_grad_() return x_adv.detach()上述代码出现TypeError: ce_loss() takes 2 positional arguments but 5 were given错误，请改正

"""Create adversarial examples using CW algorithm Args: - x: input image - model: the neural network model - loss_func: the loss function to use - c: the weight for the L2 regularization term ...
221 浏览量
filetype

All com.android.support libraries must use the exact same version specification (mixing versions can lead to runtime crashes). Found versions 28.0.0, 26.1.0. Examples include `com.android.support:animated-vector-drawable:28.0.0` and `com.android.support:mediarouter-v7:26.1.0`

你可以通过在你的项目根目录下的 build.gradle 文件中对应的 dependencies 节点中指定相同的版本来解决这个问题。例如，你可以将所有的 com.android.support 库的版本都指定为 28.0.0，或者都指定为 26.1.0。具体...
136 浏览量
filetype

idea 设置的快捷键

These are just a few examples, and the actual shortcuts may vary depending on the version and configuration of Idea. You can usually find a complete list of shortcuts in the settings or preferences ...
90 浏览量
filetype

Dev-c++目录结构

- Examples：包含一些示例程序。 - Help：包含Dev-C的帮助文件。 - Include：包含C/C++编译器所需的头文件。 - Lib：包含C/C++编译器所需的库文件。 - Plugins：包含Dev-C的插件文件。 - Templates：包含Dev-C的代码...
124 浏览量
filetype

hadoop jar /usr/local/hadoop/share/hadoop/mapreduce/hadoop-mapreduce-examples-*.jar grep input output 'dfs[a-z.]+'什么意思

- /usr/local/hadoop/share/hadoop/mapreduce/hadoop-mapreduce-examples-*.jar：Hadoop自带的MapReduce示例程序的jar包路径。 - grep：示例程序的名称，用于在输入目录中查找匹配的文本。 - input：输入目录的路径...
110 浏览量
filetype

linux系统cmd命令指导手册

Linux系统的命令指导手册通常使用man命令来查看。使用以下命令来查看任意一个命令的手册： ...- EXAMPLES：示例命令 - SEE ALSO：相关命令和文档 在手册中，使用箭头键进行滚动，按q键退出手册。
151 浏览量
filetype

做一个向客户介绍自己的软件测试团队实力的PPT

- Examples of successful projects Slide 4: Testing Methods - Title: Our Testing Methods - Overview of testing methods used (e.g. manual, automated, exploratory) - Benefits of each method Slide 5: ...
127 浏览量
菊次郎的回南天
  • 粉丝: 49
上传资源 快速赚钱

最新资源