Alloy Tutorial（2）LastPass； cacheMemory

news2025/1/11 21:40:49

文章目录

  • LastPass
    • 整体 solution 代码：
  • cacheMemory

LastPass

module LastPass

/*
 * LastPass password map
 *
 * A simple example to explain basics of Alloy. 
 *
 * The 'PassBook' keeps track of a set of users' passwords for a set of URLs. 
 * For each User/URL pair, there is one password. Passwords can be added, 
 * deleted, looked up, and changed. 
 * A user can also request all of their password for all URLs.
 *
 * author: Tim Miller; updated by Toby Murray for Alloy 6, including simplifications
 */

sig URL {}
sig Username {}
sig Password {}
sig PassBook {var password : Username -> URL -> Password}

fact NoDuplicates 
{
  always all pb : PassBook, user : Username, url : URL | lone pb.password[user][url]
}

//Add a password for a new user/url pair
pred add [pb : PassBook, url : URL, user: Username, pwd: Password] {
    no pb.password[user][url] 
    pb.password' = pb.password + (user->url->pwd)
}

//Delete an existing password
pred delete [pb : PassBook, url : URL, user: Username] {
    one pb.password[user][url]
    pb.password' = pb.password - (user->url->Password)
}

//Update an existing password
pred update [pb : PassBook, url : URL, user: Username, pwd: Password] {
    one pb.password[user][url] 
    pb.password' = pb.password ++ (user->url->pwd)
}

//Return the password for a given user/URL pair
fun lookup [pb: PassBook, url : URL, user : Username] : lone Password {
    pb.password[user][url]
}

//Check if a user's passwords for two urls are the same
pred samePassword [pb : PassBook, url1, url2 : URL, user : Username] {
    lookup [pb, url1, user] = lookup [pb, url2, user]
}

//Retrieve all of the passwords and the url they are for, for a given user
pred retrieveAll [pb: PassBook, user : Username, pwds : URL -> Password] {
    pwds = (pb.password)[user]
}

//Initialise the PassBook to be empty
pred init [pb: PassBook] {
    no pb.password
}

//If we add a new password, then we get this password when we look it up
assert addWorks {
    all pb : PassBook, url : URL, user : Username, p : Password |
        add [pb, url, user, p] => (after (lookup [pb, url, user]) = p)
}

//If we update an existing password, then we get this password when we look it up
assert updateWorks {
    all pb : PassBook, url : URL, user : Username, p, p2 : Password |
        after (lookup [pb, url, user]) = p => 
            (add [pb, url, user, p2] => (after (lookup [pb, url, user]) = p2))
}

//If we add and then delete a password, we are back to 'the start'
assert deleteIsUndo {
    all pb : PassBook, url : URL, user : Username, pwd : Password |
        (add [pb, url, user, pwd] ; delete [pb, url, user])
            => pb.password = pb.password''
}

run add for 3 but 1 PassBook
run add for 5 URL, 5 Username, 10 Password, 1 PassBook
check addWorks for 3 but 1 PassBook expect 0
check updateWorks for 3 but 1 PassBook expect 0
check deleteIsUndo for 1 but 1 PassBook

题目： Write an assertion that checks that, after running the add operation, no two users have the same password for the same URL unless that was already the case before add was run. Check this assertion on your model. Of course, this assertion is trivially false, as users should never know anything the existence of another password. The exercise is intended to have you think about how to model this assertion.


pred noSharedPasswords[pb : PassBook] {
  all user1, user2 : Username, url : URL |
    user1 != user2 => no (pb.password[user1][url] & pb.password[user2][url])
}

assert addNoSharedPasswords {
  all pb : PassBook, url : URL, user : Username, pwd : Password |
    noSharedPasswords[pb] =>
    add[pb, url, user, pwd] => after (noSharedPasswords[pb])
}

check addNoSharedPasswords for 5 but 1 PassBook expect 0
  • 这样做会出现 counter example
  • 这表明：

    出现反例表示在你的模型中存在至少一个情况，使得你的断言addNoSharedPasswords不成立。这说明，在执行 add 操作之后，即使在添加操作之前没有两个用户对同一URL有相同的密码，也可能出现两个用户对同一URL有相同的密码。
    让我们来看看可能的原因：

    • 首先，add 操作是向密码本 pb 添加一个新的用户/URL/密码组合。这并不保证新添加的密码与其他用户对同一URL的密码不同。 这意味着，如果添加的新密码与某个用户对同一URL的现有密码相同，那么 add 操作就会导致出现共享密码。
    • 因此，你的断言 addNoSharedPasswords 在当前的模型中可能不成立，这可能是由于 add 操作并未尽可能地避免添加共享密码。
    • 为了确保断言的成立，需要修改 add 操作以避免添加共享密码。例如，你可以在 add 操作中添加一个检查，确保新密码与其他用户对同一URL的密码不同。这可能会使你的模型变得复杂，但是可以提高密码的安全性。
    • 总的来说，模型的问题在于，它允许 add 操作创建共享密码，这与 addNoSharedPasswords 断言的要求相冲突。你需要修改你的模型以消除这种冲突。
  • 因此把 add 改成如下这样：
pred add [pb : PassBook, url : URL, user: Username, pwd: Password] {
    no pb.password[user][url] 
    // 在添加之前注明，新增的这个密码 pwd 不能和其他 user 的密码冲突
	all otherUser: Username | pwd != pb.password[otherUser][url]
    pb.password' = pb.password + (user->url->pwd)
}

整体 solution 代码：

module LastPass

/*
 * LastPass password map
 *
 * A simple example to explain basics of Alloy. 
 *
 * The 'PassBook' keeps track of a set of users' passwords for a set of URLs. 
 * For each User/URL pair, there is one password. Passwords can be added, 
 * deleted, looked up, and changed. 
 * A user can also request all of their password for all URLs.
 *
 * author: Tim Miller; updated by Toby Murray for Alloy 6, including simplifications
 */

sig URL {}
sig Username {}
sig Password {}
sig PassBook {var password : Username -> URL -> Password}

fact NoDuplicates 
{
  always all pb : PassBook, user : Username, url : URL | lone pb.password[user][url]
}

//Add a password for a new user/url pair
pred add [pb : PassBook, url : URL, user: Username, pwd: Password] {
    no pb.password[user][url] 
    // 对 add 操作进行限制，避免加入的时候与其他的 user 的密码重复
	all otherUser: Username | pwd != pb.password[otherUser][url]
    pb.password' = pb.password + (user->url->pwd)
}

//Delete an existing password
pred delete [pb : PassBook, url : URL, user: Username] {
    one pb.password[user][url]
    pb.password' = pb.password - (user->url->Password)
}

//Update an existing password
pred update [pb : PassBook, url : URL, user: Username, pwd: Password] {
    one pb.password[user][url] 
    pb.password' = pb.password ++ (user->url->pwd)
}

//Return the password for a given user/URL pair
fun lookup [pb: PassBook, url : URL, user : Username] : lone Password {
    pb.password[user][url]
}

//Check if a user's passwords for two urls are the same
pred samePassword [pb : PassBook, url1, url2 : URL, user : Username] {
    lookup [pb, url1, user] = lookup [pb, url2, user]
}

//Retrieve all of the passwords and the url they are for, for a given user
pred retrieveAll [pb: PassBook, user : Username, pwds : URL -> Password] {
    pwds = (pb.password)[user]
}

//Initialise the PassBook to be empty
pred init [pb: PassBook] {
    no pb.password
}

//If we add a new password, then we get this password when we look it up
assert addWorks {
    all pb : PassBook, url : URL, user : Username, p : Password |
        add [pb, url, user, p] => (after (lookup [pb, url, user]) = p)
}

//If we update an existing password, then we get this password when we look it up
assert updateWorks {
    all pb : PassBook, url : URL, user : Username, p, p2 : Password |
        after (lookup [pb, url, user]) = p => 
            (add [pb, url, user, p2] => (after (lookup [pb, url, user]) = p2))
}

//If we add and then delete a password, we are back to 'the start'
assert deleteIsUndo {
    all pb : PassBook, url : URL, user : Username, pwd : Password |
        (add [pb, url, user, pwd] ; delete [pb, url, user])
            => pb.password = pb.password''
}


pred noSharedPasswords[pb : PassBook] {
  all user1, user2 : Username, url : URL |
    user1 != user2 => no (pb.password[user1][url] & pb.password[user2][url])
}

assert addNoSharedPasswords {
  all pb : PassBook, url : URL, user : Username, pwd : Password |
    noSharedPasswords[pb] =>
    add[pb, url, user, pwd] => after (noSharedPasswords[pb])
}

check addNoSharedPasswords for 5 but 1 PassBook expect 0

cacheMemory

//Addresses and data
sig Addr {}
sig Data {}

//A cache system consists of main memory and cached memory, but mapping addresses to data
one sig CacheSystem {
	var main, cache: Addr -> lone Data
}

//Initially there is no memory allocated
pred init [c: CacheSystem] {
	no c.main + c.cache
}

//Write data to a specified address in the cache
pred write [c : CacheSystem, a: Addr, d: Data] {
	c.main' = c.main
	c.cache' = c.cache ++ a -> d
}

//Read data from a specified address in the cache
pred read [c: CacheSystem, a: Addr, d: Data] {
	some d
	d = c.cache [a]
        c.main' = c.main
        c.cache' = c.cache
}

//Load some data from the main memory in the cache
//Note that this is non-deterministic: it does not specific what to load. This is left to the implementation
pred load [c : CacheSystem] {
	some addrs: set c.main.Data - c.cache.Data |
		c.cache' = c.cache ++ addrs <: c.main
	c.main' = c.main
}

//Flush memory from the cache back into the main memory.
//Note this is also non-deterministic
pred flush [c : CacheSystem] {
	some addrs: some c.cache.Data {
		c.main' = c.main ++ addrs <: c.cache
		c.cache' = c.cache - addrs -> Data
	}
}

//If a load is performed between a write and a read, this should not be observable.
//That is, if we perform the sequence: read, write, load, and read, 
//then reading the same address in both reads should return the same value,
//unless the write in between overwrote that value (i.e. a1=a2)
assert LoadNotObservable {
	all c : CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
		{
		read [c, a2, d2];
		write [c, a1, d1];
		load [c];
		read [c, a2, d3]
		} implies d3 = (a1=a2 => d1 else d2)
	}

check LoadNotObservable for 5

题目：What is the meaning of the one and var keywords in the sig declaration?

  • one 是限制集合中元素的数量
  • var 是定义一个可变的 relation 代表其在运行途中可以发生改变（例如update 或者扩展等操作）

题目：Why does the read predicate need the following two lines? Try removing them and see how it affects the model (e.g. whether the LoadNotObservable assertion holds).
在这里插入图片描述

  • 在 Alloy 中，如果你在断言、谓词或函数中使用到带撇号（'）的变量，这表示你在引用系统的下一个状态，而不是当前状态。在这个缓存系统模型中，main' 和 cache' 分别代表下一状态的主内存和缓存内存。

  • 这两行代码的作用是确保在读取操作中，主内存和缓存内存的状态不会改变。 如果你删除了这两行，就相当于允许在读取操作中改变内存的状态，这可能会导致模型的行为与预期不符。

题目：Write an assertion called LoadPreserves, which specifies that when memory is loaded, the main memory does not change. Check this assertion.

assert LoadPreserves{
	all c: CacheSystem | load[c] => c.main'=c.main
}

check LoadPreserves

题目：Write an assertion called CannotReadInitially, which specifies that in the initial state, nothing can be read (i.e., the read operation is not valid). Check this assertion.

assert CannotReadInitially{
	all c: CacheSystem, a: Addr, d: Data | init[c] => not read[c, a, d]
}
check CannotReadInitially

Write an operation called destroy, which takes a memory address as input and removes that memory address and its associated data, whether the address is in the cache or the main memory.

pred destroy[c: CacheSystem, a: Addr]{
	c.main' = c.main - (a -> Data)
	c.cache' = c.cache - (a -> Data)
}

Write an assertion called OnlyOneMemoryDestroyed, which specifies that when memory is destroyed by the destroy operation, it removes memory from either the cache or main memory, but not both. Does this assertion hold? If not, why not?

assert OnlyOneMemoryDestroyed{
	all c: CacheSystem, a: Addr | (destroy[c, a] => c.main'=c.main-(a->Data) and c.cache'=c.cache) 
	or (destroy[c, a] =>  c.cache'=c.cache-(a->Data) and c.main' = c.main)
}

check OnlyOneMemoryDestroyed
  • 不可能 hold，因为 destroy 的定义和这个是违背的。

本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如若转载，请注明出处：http://www.coloradmin.cn/o/634818.html

如若内容造成侵权/违法违规/事实不符，请联系多彩编程网进行投诉反馈，一经查实，立即删除！

相关文章

【阿里云】第一次进行域名注册、备案以及使用全过程

【阿里云】第一次进行域名注册、备案以及使用全过程

前言 随着ChatGPT的爆火&#xff0c;让我直面感受到了一项技术的突破可以产生堪比原子弹爆炸的威力&#xff0c;因而在品尝过ChatGPT带来的便利与甜头后&#xff0c;就一直在跟进&#xff0c;同时也在能力范围内&#xff0c;让数十位朋友使用上了ChatGPT 前段时间&#xff0c…
阅读更多...
ftrace学习 —— user_events的用法

ftrace学习 —— user_events的用法

参考 https://docs.kernel.org/trace/user_events.html 测试程序 samples/user_events/example.c tools/testing/selftests/user_events/ftrace_test.c 正文 通过user_event可以实现对应用程序的跟踪&#xff0c;类似linux内核中的tracepoint那样。相似的方法还有借助/sys…
阅读更多...
走进docker

走进docker

一、Docker 概述 1、Docker的概念 • Docker是一个开源的应用容器引擎&#xff0c;基于go语言开发并遵循了apache2.0协议开源 • Docker是在Linux容器里运行应用的开源工具&#xff0c;是一种轻量级的“虚拟机” • Docker 的容器技术可以在一台主机上轻松为任何应用创建一…
阅读更多...
异常数据检测 | Python实现基于高斯概率分布的异常数据检测

异常数据检测 | Python实现基于高斯概率分布的异常数据检测

文章目录 文章概述模型描述源码分享学习小结参考资料文章概述 高斯分布也称为正态分布。它可以被用来进行异常值检测，不过我们首先要假设我们的数据是正态分布的。不过这个假设不能适应于所有数据集。但如果我们做了这种假设那么它将会有一种有效的方法来发现异常值。 模型描述…
阅读更多...
asp.net审计项目管理系统VS开发sqlserver数据库web结构c#编程Microsoft Visual Studio

asp.net审计项目管理系统VS开发sqlserver数据库web结构c#编程Microsoft Visual Studio

一、源码特点 asp.net审计项目管理系统 是一套完善的web设计管理系统&#xff0c;系统具有完整的源代码和数据库&#xff0c;系统主要采用B/S模式开发。开发环境为vs2010&#xff0c;数据库为sqlserver2008&#xff0c;使用c#语言 开发 二、功能介绍 (1)科室管理&…
阅读更多...
GIT远程仓库（随笔）

GIT远程仓库（随笔）

目录 前言 一、GIt常见命令 二、概念原理 三、常见的代码托管平台 四、配置SSH公钥 五、操作 1、注册账号 2、在gitee中&#xff0c;创建远程仓库 3、Git命令创建本地仓库 4、Git命令创建第一个版本提交 5、Git命令添加远程仓库 6、推送 7、修改开源项目 ​编辑 8、…
阅读更多...
浅谈数据库系统：MySQL的简介与安装配置

浅谈数据库系统：MySQL的简介与安装配置

前言 ✨文末送书&#xff0c;小K赠书活动第一期 目录 前言一、数据库系统概述数据(Data)数据库(Database)数据库管理系统(Database Management System,DBMS)数据库系统(Database System,DBS)什么是SQL 二、MySQL的简介与安装MySQL简介MySQL下载与安装下载解压版安装配置安装版安…
阅读更多...
前端 vue 自定义导航栏组件高度及返回箭头 自定义 tabbar 图标

前端 vue 自定义导航栏组件高度及返回箭头 自定义 tabbar 图标

前端vue自定义导航栏组件高度及返回箭头 自定义tabbar图标, 下载完整代码请访问uni-app插件市场地址:https://ext.dcloud.net.cn/plugin?id12986 效果图如下: # #### 使用方法 使用方法 // page.json 采用矢量图标设置返回箭头 ,{ "path" : "pages/Home/Ho…
阅读更多...
2023.06.11 学习周报

2023.06.11 学习周报

文章目录 摘要文献阅读1.题目2.问题3.介绍4.Problem definition5.Method5.1 Feature Extractor5.2 Synthetic Node Generation5.3 Edge Generator5.4 GNN Classifier5.5 Optimization Objective5.6 算法 6.实验6.1 数据集6.2 基线6.3 实验结果 7.结论 数学建模1.欧式距离2.切比…
阅读更多...
leetcode174. 地下城游戏(java)

leetcode174. 地下城游戏(java)

地下城游戏 leetcode174. 地下城游戏题目描述 动态规划解题思路代码 动态规划专题 leetcode174. 地下城游戏 来源&#xff1a;力扣&#xff08;LeetCode&#xff09; 链接&#xff1a;https://leetcode.cn/problems/dungeon-game 题目描述 恶魔们抓住了公主并将她关在了地下城 …
阅读更多...
python基础知识(十一):matplotlib的基本用法一

python基础知识(十一):matplotlib的基本用法一

目录 1. matplotlib库和numpy库2. matplotlib绘图的简单示例3. 设置窗口的尺寸比例&#xff0c;线宽和颜色4. 坐标轴设置5. 去除坐标轴边框和坐标轴原点化6. 图例7. 文本标注 1. matplotlib库和numpy库 matplotlib库是python的绘图库&#xff0c;numpy库是numpy是python中基于…
阅读更多...
如何使用Docker实现分布式Web自动化！

如何使用Docker实现分布式Web自动化！

1、前言 顺着docker的发展&#xff0c;很多测试的同学也已经在测试工作上使用docker作为环境基础去进行一些自动化测试&#xff0c;这篇文章主要讲述在docker中使用浏览器进行自动化测试如果可以实现可视化&#xff0c;同时可以对浏览器进行相关的操作。 如果你想学习自动化测…
阅读更多...
【动态规划专栏】-- 回文串问题 -- 动态规划经典题型

【动态规划专栏】-- 回文串问题 -- 动态规划经典题型

目录 动态规划 动态规划思维&#xff08;基础&#xff09; 状态表示&#xff08;最重要&#xff09; 状态转移方程&#xff08;最难&#xff09; 初始化&#xff08;细节&#xff09; 填表顺序&#xff08;细节&#xff09; 返回值&#xff08;结果&#xff09; 回文子串…
阅读更多...
浮点型进制转换 和 与或非（逻辑短路）

浮点型进制转换 和 与或非（逻辑短路）

正数的反码是其本身 负数的补码是其反码1 原码 十进制数据的二进制表现形式 byte b 13 1101&#xff08;13的十进制&#xff09;byte代表占存储的一个字节&#xff08;1字节等于8位&#xff09; 此时13的在存储里的形式 0000 1101 &#xff08;原码最左边0为正&#…
阅读更多...
物联网Lora模块从入门到精通(六)OLED显示屏

物联网Lora模块从入门到精通(六)OLED显示屏

一、前言 获取到数据后我们常需要在OLED显示屏上显示&#xff0c;本文中我们需要使用上一篇文章(光照与温湿度数据获取)的代码&#xff0c;在其基础上继续完成本文内容。 基础代码&#xff1a; #include <string.h> #include "board.h" #include "hal_ke…
阅读更多...
Spring boot之WEB 开发-静态资源访问--自定义转换器--处理JSON--内容协商

Spring boot之WEB 开发-静态资源访问--自定义转换器--处理JSON--内容协商

Spring boot之WEB 开发-静态资源访问 官方文档 在线文档: https://docs.spring.io/spring-boot/docs/current/reference/html/features.html#features.develo\ping-web-applications 基本介绍 1. 只要静态资源放在类路径下&#xff1a; /static 、/public 、/resources 、/M…
阅读更多...
2023-06-11：redis中，如何在100个亿URL中快速判断某URL是否存在？

2023-06-11：redis中，如何在100个亿URL中快速判断某URL是否存在？

2023-06-11&#xff1a;redis中&#xff0c;如何在100个亿URL中快速判断某URL是否存在&#xff1f; 答案2023-06-11&#xff1a; 传统数据结构的不足 当然有人会想&#xff0c;我直接将网页URL存入数据库进行查找不就好了&#xff0c;或者建立一个哈希表进行查找不就OK了。 …
阅读更多...
【Java】数组是引用类型

【Java】数组是引用类型

【Java】数组是引用类型 Java虚拟机运行时的数据区基本类型变量与引用类型变量的区别 Java虚拟机运行时的数据区 程序计数器 (PC Register): 只是一个很小的空间, 保存下一条执行的指令的地址。 虚拟机栈(JVM Stack): 与方法调用相关的一些信息&#xff0c;每个方法在执行时&a…
阅读更多...
【算法系列 | 5】深入解析排序算法之——快速排序

【算法系列 | 5】深入解析排序算法之——快速排序

序言 你只管努力&#xff0c;其他交给时间&#xff0c;时间会证明一切。 文章标记颜色说明&#xff1a; 黄色&#xff1a;重要标题红色&#xff1a;用来标记结论绿色&#xff1a;用来标记一级论点蓝色&#xff1a;用来标记二级论点 决定开一个算法专栏&#xff0c;希望能帮助大…
阅读更多...
【日志解析】【频率分析】ULP：基于正则表达式和本地频率分析进行日志模板提取

【日志解析】【频率分析】ULP：基于正则表达式和本地频率分析进行日志模板提取

An Effective Approach for Parsing Large Log Files 文章目录 An Effective Approach for Parsing Large Log Files1 论文出处2 背景2.1 背景介绍2.2 针对问题2.3 创新点 3 主要设计思路3.1 预处理3.2 日志事件分组3.3 通过频率分析生成日志模板 4 实验设计4.1 准确性4.2 效率…
阅读更多...
推荐文章
最新文章

Copyright @ 2022~2023