git rebase使用
git rebase使用
目的：用于合并多个commit，使整个commit清晰且为线性。
唯一的可能不好影响是可能让历史记录变得过于简洁，中间过程的提交不可见。
git rebase -i HEAD~4 # 合并最近四个提交commit
如果已经推到远端，当处理完commit合并后需要用git push -f 推到远端。
如果是单个commit信息需要修改则:
git commit --amend
Specifying Systems 第五章笔记
5.1 内存的接口 本节通过一个规范表示接口，不涉及实现，也即不涉及判断真假的具体公式。 首先选择抽象的层级，第二章把“发送”操作用三个变量（ val 、 rdy 、 ack ）进行描述，并把 val 和 rdy 同时更改表示为一个原子操作。本章把“发送”操作用一个变量进行描述： val 。 接口试图规定“发送”操作是某一类 动作 ，这需要描述怎样的 动作 是符合本接口的，类似于在“函数是一等公民”的编程语言中描述函数。但 TLA+ 只能把 CONSTANT 、 VARIABLE 定义的变量作为模块的参数，而不能把 动作 定义的公式作为模块的参数。作为替代，TLA+ 中可以定义运算符以达到这个目的。把 动作 涉及的 N 个变量列举出来，定义一个 N 元运算符 CONSTANTS operator_as_action(_, _, _, _) 即可。 运算符的返回值不限定类型，而 动作 是一个公式，返回值是布尔型，所以还需要一个表示类型的假设 ASSUME \A p1, p2, p3, p4 : operator_as_action(p1, p2, p3, p4) \in BOOLEAN 在学习了需要的语法知识后，我们可以定义内存的规范了。 -------------------------- MODULE MemoryInterface --------------------------- VARIABLE memInt \* represent memory CONSTANTS Send(_, _, _, _), Reply(_, _, _, _), InitMemInt, \* set of possible initial values of memInt Proc, \* set of processor identiers Adr, \* set of memory addresses Val \* se...
评论
发表评论