3 刘知昊

华东师范大学 软件工程

学生。

等级
TA的排名 2k+

【系统分析与验证学习笔记】7:有限字上正则LT性质的验证

有限自动机⇌正则语言⇌正则表达式有限自动机\rightleftharpoons正则语言\rightleftharpoons正则表达式有限自动机⇌正则语言⇌正则表达式1 有限字上的自动机1.1 有限自动机有限自动机(Finite Automata)可以表示为确定性的DFA,或者更一般的非确定的NFA:A=(Q,Σ,σ,Q0,F)A=(Q, \Sigma, \sigma, Q_0, F)A=(...

2019-12-02 10:41:49

【Bison学习笔记】1:生成简易的语法分析程序,使Bsion和Flex协同工作

简述Bison是在Yacc上改写并添加了大量特性后诞生的语法分析生成器,在编译前端(词法分析->语法分析->语义分析)中处在中间的位置,它可以用来生成特定的语法分析程序。安装Bison:apt-get install bison没有专用于Bison的IDE,可以在VSCode安装Lex Flex Yacc Bison插件,可以让Bison语法高亮。Bsion和Flex协同工...

2019-12-01 16:45:36

【Flex学习笔记】1:生成简易的词法分析程序

简述Flex是重写Lex诞生的快速词法分析生成器,在编译前端(词法分析->语法分析->语义分析)中处在最靠前的位置,它可以用来生成特定的词法分析程序。安装Flex:apt-get install flex没有专用于Flex的IDE,可以在VSCode安装Lex Flex Yacc Bison插件,可以让Flex语法高亮。Flex使用示例Flex程序通常写成.l文件,其中由...

2019-12-01 00:27:18

【系统分析与验证学习笔记】6:线性时序性质(Linear-time Properties)

为方便,线性时序性质(linear-time properties)后续均简称LT性质。在系统分析中,描述线性时序行为(linear-time behavior)可以是基于动作的(action-based approach),也可以是基于状态的(state-based approach),本章主要学习的是基于状态的(但在学习公平性时用动作描述),也就可以在TS中刻意忽略转移过程中的具体动作,而只...

2019-11-04 14:49:37

【WebGME学习笔记】1:配置和使用WebGME

配置WebGME环境整体和配置使用Vue的时候很像。注意WebGME需要事先安装和启动本地的MongoDB服务。安装webgme-cli脚手架:npm install -g webgme-cli配置自动补全,打开WSL命令行,执行:echo ". G:\Program Files\nodejs\node_global\node_modules\webgme-cli\extra\webg...

2019-10-20 14:37:48

【进程代数学习笔记】4:[CSP]进程间的通道通信,管道与活锁避免

1 记号1.1 通道和数据同系统分析与验证课上学的Channel system记号类似,CSP中用序偶c.vc.vc.v(参见笔记一的2.14)表示在通道ccc上传送数据vvv。则进程PPP能够在通道ccc上通信的数据记为:αc(P)={v ∣ c.v∈αP}\alpha c(P) = \{v \ | \ c.v \in \alpha P \}αc(P)={v ...

2019-10-20 15:49:39

【系统分析与验证学习笔记】5:PG向TS的转换,进程并发的几种模型

1 PG向TS的转换在上节学习的数据依赖的系统中使用PG对系统进行了建模,在其他的场景下,如后面要学习的某些特殊的进程并发场景,也需要用PG对系统建模,将其转换成TS表示对实际实现是重要的。PG六元组:PG=(Loc,Act,Effect,↪,Loc0,g0)PG=(Loc,Act,Effect,\hookrightarrow,Loc_0,g_0)PG=(Loc,Act,Effect,↪,L...

2019-10-19 09:39:36

【进程代数学习笔记】3:[CSP]进程与不确定性

前面一二章所学习的进程分裂或协作的方式有:选择(P∣QP|QP∣Q):用于和环境交互,由环境(CSP里亦用进程表示)选择当前动作以决定进程接下来的分支。并发(P∣∣QP||QP∣∣Q):用于进程间的协作,或用于为进程施加影响它的环境进程。如上面所述的,一条竖线表达的选择即是确定性(deterministic)选择,确定性选择是环境能把控的。与之相对地可以引入不确定性(nondeterm...

2019-10-18 19:23:57

【进程代数学习笔记】2:[CSP]进程的并发执行与相关操作

1 并发(concurrency)与死锁1.1 例子如课本P8的复杂贩卖机进程:VMC=(in2p→(large→VMC∣small→out1p→VMC)∣in1p→(small→VMC∣in1p→(large→VMC∣in1p→STOP)))VMC = (in2p \to (large \to VMC | small \to out1p \to VMC) \\| in1p \to (s...

2019-10-14 14:43:53

【进程代数学习笔记】1:[CSP]进程的基本表示,迹及其操作

1 进程的基本表示进程的普适表示是(x:A→P(x))(x:A \to P(x))(x:A→P(x)),意为选择字母表AAA中一动作xxx,在PPP执行过xxx这一动作后接下来的行为记作P(x)P(x)P(x)。A=αPA=\alpha PA=αP表示进程PPP的动作集合。STOPASTOP_ASTOPA​表示无法执行任何动作的进程(注意AAA不同STOPASTOP_ASTOPA​不同,但仅...

2019-10-13 19:01:41

【SciKit-Learn学习笔记】9:常用的特征编码手段

在Kaggle上看到了一个专门训练特征编码的竞赛,其中一个Kernel讲了常用的几种特征编码的手段,基于这篇教程做了些扩展学习。用于数据分析的特征可能有多种形式,需要将其合理转化成模型能够处理的形式,特别是对非数值的特征,特征编码就是在做这样的工作。常见特征种类二值数据:只有两种取值的变量(不一定是0/1,但是可以映射到{0,1}\{0,1\}{0,1}上)类别数据:多类的数据,如星期一...

2019-10-04 22:44:37

【系统分析与验证学习笔记】4:基于TS以及Program Graph的软硬件系统建模

在TS中“变量”一词要以广义的方式理解,可以表示程序变量、程序计数器、寄存器值、输入位等。1 顺序硬件电路的建模1.1 一个简单的例子1.1.1 简要分析下面电路有输入xxx,寄存器rrr和输出位yyy:其中:λy=¬(x⊕r)δr=x∨r\lambda_y = \neg (x \oplus r) \\\delta_r = x \vee rλy​=¬(x⊕r)δr​=x∨r在...

2019-09-30 20:11:32

【系统分析与验证学习笔记】3:基于Transition System的系统模型

TS是一种常用的描述系统行为的模型,用结点表示状态,边表示转移关系,和KS的主要区别是状态转移是需要动作支持的,不同的动作往往对应着不同的状态转移。1 基本概念1.1 状态(State)状态是在某时刻系统所具有的特性和行为。和KS一样用原子命题集合表示状态,例如{a=2,b>3}\{a=2,b>3\}{a=2,b>3}。对交通灯而言,灯的颜色就是状态。对顺序程序而言,...

2019-09-26 13:51:35

【系统分析与验证学习笔记】2:基于Kripke Structure的系统模型

形式化模型的构建思路舍弃和性质无关的细节,保留系统中的关键属性。如对于电路而言,各个门和布尔值是需要关心的,而电压是不关心的。对于通信协议而言,信息的交换过程是需要关心的,而具体交换的信息是和建模没关系的。本章学习的是对响应式系统(reactive system)以及它随时间的行为的建模,响应式系统会和环境进行交互,并且一般不会终止。State:在某一特定时刻系统中所有变量的取值,表征...

2019-09-24 16:18:01

【系统分析与验证学习笔记】1:系统分析与验证概览

验证方法模拟:动态验证,常用,如今最主流的验证方法。仿真:类似模拟,但依赖于硬件。形式化验证:静态验证,用数学方法对模型的功能、功能、规范做检验。验证的完备性高,但实施困难。半形式化验证:形式化验证和前面结合。形式化验证分类按验证内容分类性质检验(property checking):是否满足某些规范和功能需求。等价性验证(equivalence verification):...

2019-09-24 07:32:18

【Nginx学习笔记】3:配置文件的语法,命令行的使用(重载配置文件,热部署,切割日志文件)

Nginx二进制文件中已经指定了Nginx包含了哪些模块,所有模块有独立的配置,但遵循相同的配置语法。Nginx配置文件语法基本规则有些指令块可以有参数(跟在指令块名后面),有些指令块不能有参数,具体是由提供指令块的Nginx模块来决定的。时间单位后缀空间单位后缀一个例子Nginx命令行的使用简述Nginx命令行和大多Linux命令是类似的,格式是nginx -参数 参数...

2019-08-19 16:44:51

【算法学习笔记】4:贪心法,回溯法,分支限界法,解空间树剪枝

[4]贪心算法贪心算法不从整体最优上考虑,而是在局部最优上做出选择。对于很多问题贪心法不能得到整体最优解,但对于某些特殊的问题,仍然可以得到整体最优解。使用贪心算法应满足这些性质: ①最优子结构性质:一个问题的最优解包含的子问题也是最优的。 ②贪心选择性质:整体最优解可以通过一系列局部最优的选择,即贪心选择来达到。活动安排问题n个活动的集合E,都需要使用同一资源,活动i有开始时间si和

2019-08-17 22:38:09

【Nginx学习笔记】2:Nginx的版本发布情况,选择哪种Nginx,安装符合自己需求的Nginx

版本发布情况在Nginx开源版官网点击右侧download可以看到各个版本的Nginx,其中Mainline是抢先的主干版本(版本号是奇数),Stable是稳定版(版本号是偶数)。点击某个版本左侧的CHANGES可以查看CHANGES文件,其中Feature标注了新增的功能,Bugfix标注了修复的bug,Change标注了做了重构的部分。选择哪种Nginx没有特殊需求一般就用开源版Ngi...

2019-08-17 22:32:37

【Nginx学习笔记】1:Nginx的使用场景,出现背景,优点,组成部分

Nginx的使用场景[1]反向代理服务应用服务对开发效率要求很高,其使用效率(QPS,TPS等)是非常有限的,所以需要很多应用服务构成集群,这时候就要用到Nginx的反向代理功能,将动态请求传给各个应用服务。这些应用服务构成集群后至少又会产生两个需求:动态扩容容灾处理(服务可能会出问题)所以Nginx反向代理要有负载均衡的功能。另外,Nginx往往处在企业内网的边缘,随网络链路...

2019-08-14 15:33:48

【MATLAB学习笔记】1:基本操作技巧和矩阵的使用

特殊变量和常量使用iskeyword命令可以看到众关键字,但还有些特殊变量和常量也不能作为标识符来使用。ans:最近一次计算的结果i,j:用于表示复数Inf(即inf):无穷大,试计算1/0和log(0)将分别得到正负无穷大eps:表示浮点数的相对精度,浮点数越靠近0精度越大,MATLAB无法表示1至1+1eps之间的数,也无法表示2至2+2eps之间的数NaN:Not a Numb...

2019-07-24 22:07:36

查看更多

勋章 我的勋章
  • 领英
    领英
    绑定领英第三方账户获取
  • GitHub
    GitHub
    绑定GitHub第三方账户获取
  • 脉脉勋章
    脉脉勋章
    绑定脉脉第三方账户获取
  • 签到新秀
    签到新秀
    累计签到获取,不积跬步,无以至千里,继续坚持!
  • 专栏达人
    专栏达人
    授予成功创建个人博客专栏的用户。专栏中添加五篇以上博文即可点亮!撰写博客专栏浓缩技术精华,专栏达人就是你!
  • 持之以恒
    持之以恒
    授予每个自然月内发布4篇或4篇以上原创或翻译IT博文的用户。不积跬步无以至千里,不积小流无以成江海,程序人生的精彩需要坚持不懈地积累!
  • 1024勋章
    1024勋章
    #1024程序员节#活动勋章,当日发布原创博客即可获得
  • 勤写标兵Lv2
    勤写标兵Lv2
    授予每个自然周发布4篇到6篇原创IT博文的用户。本勋章将于次周周三上午根据用户上周的博文发布情况由系统自动颁发。