Alloy Tutorial(2)LastPass; cacheMemory

news/2024/10/31 3:20:16/

文章目录

  • 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.mainc.cache' = c.cache ++ a -> d
}//Read data from a specified address in the cache
pred read [c: CacheSystem, a: Addr, d: Data] {some dd = c.cache [a]c.main' = c.mainc.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.mainc.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.cachec.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.ppmy.cn/news/332199.html

相关文章

浮点型进制转换 和 与或非(逻辑短路)

正数的反码是其本身 负数的补码是其反码1 原码 十进制数据的二进制表现形式 byte b 13 1101&#xff08;13的十进制&#xff09;byte代表占存储的一个字节&#xff08;1字节等于8位&#xff09; 此时13的在存储里的形式 0000 1101 &#xff08;原码最左边0为正&#…

Android手机电池耐用吗,手机电池是否还耐用?一招教你识别

原标题&#xff1a;手机电池是否还耐用&#xff1f;一招教你识别 现如今的智能手机遍布&#xff0c;都是锂离子电池&#xff0c;由于锂离子的特性会导致在充电放电间会产生损耗。 一般情况&#xff0c;锂电池循环充电次数达到300至500次后&#xff0c;电池的容量就会下降到最初…

锂电池电压和电量的关系

锂电池电压和电量之间,有一定的对应关系,通过对开路电压的测量,可以大致得出电池的剩余电量。不过用电压测量电量的方式有一定的不稳定性,例如放电电流、环境温度、循环、放电平台、电极材料等,都会给最后结果的准确与否带来影响。 电压和电量的对应关系是: 100%----4.…

常用的锂电池充电芯片

1.TP4056——UMW(友台半导体) TP4056是一款性能优异的单节锂离子电池恒流/恒压线性充电器。 TP4056采用ESOP8封装配合较少的外围原件使其非常适用于便携式产品&#xff0c;并且适合给USB电源以及适配器电源供电。 基于特殊的内部MOSFET架构以及防倒充电路&#xff0c;TP4056不…

手机电池的超强攻略

如何辨别手机电池是否完全激活 1、电池充电速度十分快&#xff0c;1个多小时甚至不到一小时充电显示量就已达到100%。 2、充电达100%后&#xff0c;拔掉充电插头&#xff0c;后在插上时充电显示量回落到50%-80%. 3、充电达100%后&#xff0c;开机手机电池显示量并未满格&#x…

鸿蒙王者荣耀想要转区吗,王者荣耀转区功能怎么设置 王者荣耀角色迁移设置方法...

王者荣耀转区功能怎么设置&#xff1f;所谓的转区功实际上就是角色迁移功能&#xff0c;这是王者荣耀S18赛季中新出的一个功能&#xff0c;可以让玩家们实现转区。下面就是王者荣耀角色迁移设置方法了&#xff0c;想要换区的小伙伴们都来看看吧&#xff01; 王者荣耀转区功能怎…

王者荣耀转区仅显示可转移服务器,王者荣耀怎么转区 王者荣耀转区方法大全...

王者荣耀怎么转区呢&#xff1f;很多玩家都有转区的念头&#xff0c;不过都苦于不知道转区的方法&#xff0c;下面就让小编来告诉大家吧。 最近很多玩王者荣耀的玩家应该都听说了可以转区了&#xff0c;很多人都跃跃欲试&#xff0c;这个功能目前还在测试阶段&#xff0c;而且只…

wifi服务器延迟高,王者荣耀延迟过高怎么办?王者荣耀wifi延迟解决方法

王者荣耀wifi延迟高怎么办&#xff1f;王者荣耀太卡进不去怎么办&#xff1f;希望这篇王者荣耀太卡进不去解决办法&#xff0c;能够帮到正在玩王者荣耀的玩家朋友。 玩家想要在战斗中获得胜利&#xff0c;首要的条件就是我们延迟要在合理的范围内&#xff0c;不然的话我们连技能…