定义一个颜色选择的ComboBox
代码中要实现一个颜色选择的下拉框,从Qt的例子中找到一个。记录下来。这段代码的核心是,正如在Model/View中提到的,QCombox等内部都使用了Model。这是一个例子。看到这个例子,可以对Model/View有了更深刻的理解。
定义一个颜色选择的ComboBox来自Qt的例子程序 coloreditorfactory的一部分, 演示如何创建一个选择颜色的下拉框. 它产生一个使用颜色名的下拉框, 并且使用对应的颜色作为每一项的背景色.
QComboBox后台使用了Model, 因此, 我们设置其Qt::DecorationRole来产生颜色效果.
1234567891011121314151617181920212223242526272829303132333435363738class ColorListEditor : public QComboBox{ Q_OBJECTpublic: ColorListEditor(QWidget *widget=nullptr); QColor color() const; ...
第9章 状态机
第9章 状态机9.1 状态机
第8章 数据结构
出差回来今天找项目组聊了一下,他们最近跑去终端的人不少。问了一下现在5G这块问题多不多,说还是挺多的,设计遗漏还是不少,天天都在开会。不过我负责的设备组网,载波配置,软件管理这三块没啥问题,人都被调去支援其他的人了。那就好。反正我也快要走人了。走了之后留一摊子问题让后人解决就太丢人了。最好是现在这样,我出去一个月没人找还没有问题。
第8章 数据结构linked list,LL,链表
8.1 规格定义TLA中,一般把数据结构表示为函数或结构(它实际也是函数)。为了方便,module应有一个叫LinkedLists(Nodes)的operator,来生成所有的有效的链表集合。它是一个function set形式:[Nodes -> Nodes]
一步步来先定义所有可能的结点的映射:
12PointerMaps(Nodes) == [Nodes -> Nodes] LinkedLists(Nodes) == \* ...
然后考虑链尾(final node),它指向一个null,因此我们要定义NULL,在CONSTANT 里定义,并且要确保没有结点为NULL一一需要断言,使用 ...
第7章 算法验证
这两天又在扯速率协商的事情!
第7章 算法验证这一章会讲述如何用TLA+编写和验证算法。所谓验证算法,指的是算法会终止且输出结果,而不是一直跑下去或不断与环境交互
7.1 单过程(Single-Process)算法模板:
123456789101112131415161718---- MODULE name ---- EXTENDS \* whatever Expected(input) == \* ...Helpers == \* ...(*--algorithm name variables input \in \* ... output; \* ... \* helper variables begin \* algorithm implementation assert output = Expected(input); end algorithm; *) ====
内容:
Expected
Helpers
inputs
output
7.2 Max7.2.1 算法分析设计计算一个sequence的最大值。例 ...
第6章 时间逻辑Temporal Logic
第6章 时间逻辑Temporal Logic检查程序本身的行为(原文中叫behavior)。
算法是否总能结束(terminate)
队列中的消息是否都能得到处理
当受到扰乱(disrupted)时,系统是否能够最终回到稳定的状态
数据库是否满足最终一致性
6.1 终止Termination检查算法是否最终能停止,而不会crash或陷入死循环
6.1.1 红绿灯的例子一辆车和一个红绿灯,分别是两个process:traffic light切换信号灯,car在灯变绿之前一直等待
1234567891011121314151617181920212223extColor(c) == CASE c = "red" -> "green" [] c = ”green“ -> ”red“(*--algorithm traffic variables at_light = TRUE, ❓at_light这个变量的作用不理解 light = ”red“; proc ...
第5章 并发
第5章 并发在并发(concurrent )系统中,没有单一的timeline 。两个概念:process, label
5.1 Label标签标签决定了规格中的原子性的粒度(grain of atomicity)TLC一"步(Step)"执行完一个标签定义的内容,然后检查所有的不变量并找出下一个可能要执行的所有的标签并进行测试。
⚠️不知是不是我的理解有错误。原文:Labels determine the grain of atomicity of your spec. TLC executes everything in a label in a single step, or action. Then it checks all invariants and looks for the next label to execute (action to take).这里的问题是,当标签内又有标签时点样行为?一个single step里执行最内层的标签还是最外层的?
pc,指的是"program counter",指的是当前所在的标签。
可以用goto 在本process 中跳转 ...
第三章 Operator和Function
第3章 Operator和Function
它的叫法很别扭,Operator以后叫"算子",Function 还叫"函数"。真难受!
3.1 Operator有些类似于一般编程语言中的函数/过程。无参数时不用写用==定义:
Op(arg1, arg2) == Expr
Op == Expr
它可以当宏用,也可以当变量用
垃圾桶例子中的改进:
若要在算子中用PlusCal算法中定义的变量,则要把它放在define块中:必须在宏定义之前,变量定义之后。
/\的特别的用法为了美观,第一个前面也可以放一个/\或\/这种:
缩进表示嵌套括号:
算子中支持Lambda和高阶函数LAMBDA和高阶函数
12345678Add(a, b) == a + b Apply(op(_, _), x, y) == op(x, y) >> Apply(Add, 1, 2) >> 3Apply(LAMBDA x, y: x + y, 1, 2) >> 3
集合++和—123set ++ elem == set \union {e ...
第4章 Constant, Model, Import
第4章 Constant, Model, Import
这一章主要是使用。不对着工具很难记得住,不是很重要,记住几个概念就可以了。
PlusCal
第2章 PlusCal2.1 介绍2.2 定义规格2.2.1 规格的布局
在MODULE前后各至少要有四个-,由至少四个=结尾
模块名必须和文件名相同
EXTENDS导入外部模块,这里导入了Integers
\*是行注释,(* ... *)是TLA的块注释。PlusCal写在TLA的块注释中(这样TLA的解释器会忽略它),并由- -algorithm <name>开始,由algorithm结尾。algorithm的名字不需要和文件名一样
在algorithm中,用variables标示初始化变量,变量之间用,隔开
我们在这里写我们的算法
2.2.2 表达式在TLA中,一切要么是表达式Expressions,要么是操作子operator。
expression evaluator
2.2.3 值基本值类型TLA支持的值类型:string, integer, Boolean, 以及模型值(model value)。不支持浮点数
支持的操作:
注意=和:=的区别:
=是相等比较,:=是赋值
在纯粹的TLA中,只有相等比较,没有赋值。若x已初始化了并想将其与1比较,用x ...
后记
大概是因为安全的事情, 公司安全一下子搞得特别认真.
那天看到一篇亚马逊使用TLA来做形式化验证的文章, 对TLA感兴趣了, 就找到这本入门的书看了一下. 这本书纯粹是一个DSL语言和工具的使用, 实际上并没有牵涉到太多的数学的东西. 只要能看懂函数式语言, 基本上都能够看懂. 但是担心不用就会忘了, 所以当笔记一样把比较重要的东西给翻译了一下.
但是, 这个东西其实还是只适用于算法的验证, 而不是什么业务流程的实现和代码的验证.
后来我们联系了华东师大的一位做形式化设计的著名教授来交流过一次,他参与过上海地铁的软件设计。那个是真的需要形式化来证明软件的正确性。但是了解下来感觉,即使是华为,像我们这种需要7x24x356连续工作的RRU设备,用形式化也太奢侈了。即使是RRU这种相对规模比较小的产品,也超过了80万行代码,根本不可能搞什么形式化。至于人员能力水平就更不要提了,或许只有计算机科学科班出身的才知道这个是什么,像我们这种半路出家的都需要重新学习。
这个东西也就是在华为这种公司有意义,离开了之后,一般的企业根本达不到这个级别。就是屠龙技了。