天道酬勤,学无止境

How can i change these into CTL SPEC in NuSMV model?

I need help writing these CTL. I don't reall understand how to write in NuSMV format yet, hopefully my code will make sense to you since it is incomplete atm.

2)If a process is waiting, it will eventually get to its critical section

3)The two processes must 'take turns' entering the critical section

4)It is possible for one process to get into the critical section twice in succession (before the other process does).

5)Successive entries into a critical section by process 1 will be separated by at least n cycles, where n is some constant. You should choose an appropriate value for n, and this one should be verified (i.e., not disproven).

6)2 more non-trivial properties of your choice

MODULE thread1(flag2,turn)
VAR
   state : {W0,F1,W1,T1,F2,Wait,F3,C1,T2,F4};
   flag1 : boolean;

ASSIGN
   init(state) := W0;
   next(state) :=
case
   state = W0                 : F1;  
   state = F1                 : W1;  
   state = W1 & flag2         : T1; 
   (state = W1) & !flag2      : C1;  
   (state = T1)&(turn = 2)    : F2;  
   (state = T1)&(turn != 2)   : W1;  
   (state = F2)               : Wait; 
   (state = Wait)&(turn = 1)  : F3;   
   (state = Wait)&(turn != 1) : Wait; 
   (state = F3)               : W1; 
   (state = C1)               : T2; 
   (state = T2)               : F4; 
   (state = F4)               : W0;
    TRUE : state;
esac;

init(flag1) := FALSE;
next(flag1) := 
case
   state = F1 | state = F3 : TRUE;  
   state = F2 | state = F4 : FALSE; 
   TRUE                    : flag1;
esac;

DEFINE
  critical := (state = C1);
  trying := (state = F1 | state = W1 | state = T1 | state = F2 |     state = Wait | state = F3);  

MODULE thread2(flag1,turn)
VAR
   state1 : {N0,N1,N2,N3,N4,Wait1,N5,Critical1,N7,N8};
   flag2 : boolean;

ASSIGN
   init(state1) := N0;
   next(state1) :=
case
   (state1 = N0)               : N1;  
   (state1 = N1)               : N2;  
   (state1 = N2) & flag1       : N3;  
   (state1 = N2) & !flag1      : Critical1;
   (state1 = N3) & (turn = 1)  : N4;  
   (state1 = N3) & (turn != 2) : N2;  
   (state1 = F4)               : Wait1; 
   (state1 = Wait1)&(turn = 2) : N5;   
   (state1 = Wait1)&(turn != 2): Wait1; 
   (state1 = N5)               : N2; 
   (state1 = Critical1)        : N7; 
   (state1 = N7)               : N8;
   (state1 = N8)               : N0;
    TRUE : state1;
esac;

init(flag2) := FALSE;
next(flag2) := 
case
   state1 = N1 | state1 = N5 : TRUE;  
   state1 = N4 | state1 = N8 : FALSE;
   TRUE                    : flag2;
esac;

DEFINE
  critical := (state1 = Critical1);
  trying := (state1 = N1 | state1 = N2 | state1 = N3 | state1 = N4 |     state1 = Wait1 | state1 = N5);  

MODULE main

VAR

turn: {1, 2};
proc1: process thread1(proc2.flag2,turn);
proc2: process thread2(proc1.flag1,turn);

ASSIGN

init(turn) := 1;
next(turn) := 
case
   proc1.state = T2 : 2;
   proc2.state1 = N7 : 1;
   TRUE : turn;
esac;

SPEC 

AG !(proc1.critical & proc2.critical); 
--two processes are never in the critical section at the same time

SPEC 
AG (proc1.trying -> AF proc1.critical);

评论

Note: giving you a comprehensive introduction to CTL in an answer is quite unrealistic. In addition to this quick and dirty course on NuSMV/nuXmv, you might benefit from looking at these slides, which provide a theoretical background on CTL Model Checking.


CTL OPERATORS

Assume that for simplicity your program has a unique initial state.

The semantics of the CTL operators is the following:

  • AF P: in all possible execution paths, sooner or later P will be true.
  • AG P: in all possible execution paths, P is always true.
  • AX P: in all possible execution paths, in the next state P is true.
  • A[P U Q]: in all possible execution paths, P is true * until Q is true (at least once).

  • EF P: in at least one execution path, sooner or later P will be true.

  • EG P: in at least one execution path, P is always true.
  • EX P: in at least one execution path, in the next state P is true.
  • E[P U Q]: in at least one execution path, P is true * until Q is true (at least once).

*: until is true also on a path in which P is never true, provided that Q is immediately verified. [Also, see: weak/strong until]

If you have multiple initial states, then the CTL property holds if it is true for every initial state.


Properties:

Note that since your NuSMV model is currently broken and this appears to be a homework, I will provide you with a pseudo-code version of the properties and leave it to you to fit them on your own code.

  • if a process is waiting, then it will eventually get to its critical section

    CTLSPEC AG (proc1.waiting -> AF proc1.critical);
    

    explanation: the content of the parenthesis encodes exactly the sentence as you read it. I added AG because the property must clearly hold for every possible state in your model. If you omit it, then the model checker will simply test whether proc1.waiting -> AF proc1.critical is true in your initial state(s).

  • the two processes must 'take turns' entering the critical section

    CTLSPEC AG ((proc1.critical -> AX A[!proc1.critical U proc2.critical]) &
               (proc2.critical -> AX A[!proc2.critical U proc1.critical]));
    

    explanation: let me premise that this encoding works because both proc1 and proc2 stay in the critical section for only one state. The idea of proc1.critical -> AX A[!proc1.critical U proc2.critical] is the following: "if process 1 is in the critical section, then starting from the next state process 1 will never be in the critical section (again) until when process 2 is in the critical section".

  • It is possible for one process to get into the critical section twice in succession (before the other process does).

    CTLSPEC EF (proc1.critical -> EX A[!proc2.critical U proc1.critical]);
    

    explanation: similar to the previous one. Here I use EF because it suffices the property holds just once.

  • Successive entries into a critical section by process 1 will be separated by at least n cycles, where n is some constant. You should choose an appropriate value for n, and this one should be verified (i.e., not disproven).

    edit: I removed this encoding because on a second thought the formula I wrote is much stronger than required. However, I don't think it's possible to weaken it with the E operator, as it would become much weaker than required. At the time being I can't think of a possible alternative other than modify your model to count the number of cycles, whatever that means.

受限制的 HTML

  • 允许的HTML标签:<a href hreflang> <em> <strong> <cite> <blockquote cite> <code> <ul type> <ol start type> <li> <dl> <dt> <dd> <h2 id> <h3 id> <h4 id> <h5 id> <h6 id>
  • 自动断行和分段。
  • 网页和电子邮件地址自动转换为链接。

相关推荐
  • 如何在 NuSMV 中创建一个简单的 Kripke 模型?(How to create a simple Kripke model in NuSMV?)
    问题 我目前正在做一些关于 LTL(线性时间时序逻辑)和 CTL(计算树逻辑)的理论研究。 我是 NuSMV 的新手,我很难创建一个简单的 Kripke 结构。 我的结构是 M = (S, R, L) 其中 S = {s0, s1, s2} 是可能状态的集合,R 是一个转换关系,使得: s0 -> s1, s0 -> s2, s1 -> s0、s1 -> s2 和 s2 -> s2,L 是每个状态的标记函数,定义为:L(s0) = {p, q}, L(s1) = {q, r}, and L( s2) = {r}。 我正在使用 Huth 和 Ryan 在 Logic in Computer Science 教科书中描述的符号。 我尝试了以下两个代码: 第一段代码: MODULE main VAR p : boolean; q : boolean; r : boolean; state : {s0, s1, s2}; ASSIGN init(state) := s0; next(state) := case state = s0 : {s1, s2}; state = s1 : {s2}; state = s2 : {s2}; esac; init(p) := TRUE; init(q) := TRUE; init(r) := FALSE; next(p) := case state
  • How to create a simple Kripke model in NuSMV?
    I am currently doing some theoretical research in LTL (Linear-time Temporal Logic) and CTL (Computation Tree Logic). I am new to NuSMV and I have difficulty to create a simple Kripke structure. My structure is M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan. I have tried two following codes: The
  • 如何使用NuSMV见证中间人攻击(Needham-Schroeder协议)?(How to use NuSMV to witness the man-in-the-middle attack (Needham-Schroeder protocol)?)
    问题 我有以下简化的公钥 Needham-Schroeder 协议: A → B: {Na, A} Kb B → A: {Na, Nb} Ka A → B: {Nb} Kb 其中Na , Nb是A , B的随机数, Ka , Kb分别是A , B公钥。 由一方的公钥加密的消息只能由一方解密。 在步骤(1), A通过发送随机数和其身份(通过加密的协议B的公钥)至B 。 B使用其私钥解密该消息并获得A的身份。 在步骤 (2) 中, B将A及其随机数(由A的公钥加密)发送回A 。 A使用其私钥对消息进行解码并检查其随机数是否被返回。 在步骤 (3) 中, A将B的随机数(由B的公钥加密)返回给B 以下是对上述简化协议的主要中间人攻击: (1A) A → E: {Na, A} Ke ( A想和E说话) (1B) E → B: {Na, A} Kb ( E想说服B是A ) (2B) B → E: {Na, Nb} Ka ( B返回由Ka加密的随机数) (2A) E → A: {Na, Nb} Ka ( E将加密消息转发给A ) (3A) A → E: {Nb} Ke ( A确认它正在与E交谈) (3B) E → B: {Nb} Kb ( E返回B的随机数) 我希望在发现攻击时,提出了一个修复程序来防止攻击( B将其身份与随机数一起发送回A ): A → B: {Na, A} Kb B → A
  • 在 Java 中使用 NuSMV 作为模型检查器(Employing NuSMV as a model checker in java)
    问题 我正在尝试使用 NuSMV 作为 Java 中的模型检查器。 但是,我无法在线找到相关的 JAR 库。 我找到的唯一一个在这里提供,下载链接不再起作用。 显然,图书馆存在,但访问链接不起作用。 有谁知道我如何访问 NuSMV java API 库或知道任何替代方法? 回答1 这是来自同一作者的nusmv-tools的有效下载链接,包括您正在谈论的Java前端: https://code.google.com/archive/a/eclipselabs.org/p/nusmv-tools/downloads 我还没有测试过这个库,我只是验证了它可以下载。
  • Employing NuSMV as a model checker in java
    I'm trying to use NuSMV as a model checker in java. However, I'm not able to find the related JAR library online. The only one I've found is provided on here for which the download link doesn't work anymore. Apparently, the library exists but the access link is not working. Does anyone know how I can access NuSMV java API library or know of any alternative way?
  • Numbers Lite 游戏的模型检查(Model Checking For Numbers Lite Game)
    问题 我正在研究模型检查方法,我想使用这些技术来解决一个名为 Numbers Paranoia lite 的游戏规划问题。 给定一个MxN ,(MxN > 8),矩阵中的每个板块是问题图像 - 空 - 由一个从 1 到 8 的唯一数字标识 目标是找到一条路径,从标有 1 的盘子开始,覆盖矩阵中的所有盘子,并在标有 8 的盘子上结束。 有效路径中的所有非空盘子必须按从 1 到8. 我对将游戏建模为过渡状态并运行NuSMV以获得结果感到困惑。 这是我的解决方案 --·¹º§ : 01 MODULE main VAR rec: {101,102,103,104,105,106,107,201,202,203,204,205,206,207,301,302,303,304,305,306,307,401,402,403,404,405,406,407,501,502,503,504,505,506,507}; ASSIGN init(rec) := 101; next(rec) := case rec = 101 : {102, 201}; rec = 102 : {101,202,103}; rec = 103 : {102,203,104}; rec = 104 : {103, 204,105}; rec = 105 : {104,205,106}; rec = 106 : {105
  • NuSMV 模型检查中的错误?(Bug in NuSMV Model Checking?)
    问题 假设我有以下结构 M = (S, R, L) 其中 S = {s0, s1, s2} 是可能状态的集合,R 是一个转换关系,使得: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2,L 是每个状态的标记函数,定义为:L(s0) = {p, q}, L(s1) = {q, r},和L(s2) = {r}。 我正在使用 Huth 和 Ryan 在 Logic in Computer Science 教科书中描述的符号。 显然,从这样的模型中,我们有 X r 在 s0(初始状态)中得到满足,因为 r 在 s1 和 s2 中得到满足。 我的 Kripke 结构的 NuSMV 代码如下(如此处所述)。 MODULE main VAR p : boolean; q : boolean; r : boolean; state : {s0, s1, s2}; ASSIGN init(state) := s0; next(state) := case state = s0 : {s1, s2}; state = s1 : {s2}; state = s2 : {s2}; TRUE : state; esac; init(p) := TRUE; init(q) := TRUE; init(r) := FALSE; next(p) :=
  • Bug in NuSMV Model Checking?
    Suppose I have following structure M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan. Clearly, from such model, we have X r is satisfied in s0 (the initial state), since r is satisfied in s1 and s2. My NuSMV code for the Kripke structure is as follows (as described here). MODULE main VAR p
  • Golang在Kubernetes语境下的编程范式
    前言 本文根据Gopher Meetup杭州站嘉宾张磊的演讲进行整理,演讲主题为《Kubernetes语境下基于Golang的编程范式》,本文将从如下几个方面介绍: 1、Kubernetes项目选择Golang的原因 2、Kubernetes的设计模式 3、Controller Demo 演示 4、Kubernetes项目的编程范式 5、总结 Kubernetes项目为什么选择Golang? 第一部分首先什么是Kubernetes。Kubernetes的定位是非常明确和简单,就是容器的编排与调度管理的框架,它是由谷歌发起的,也是谷歌Borg/Omega项目的开源衍生项目。它是目前世界上开源项目中最流行的项目之一(Linux排第一,Kubernetes排第四),这也就意味着它的社区活跃度以及项目的发展速度是相当高。像这样一个快速迭代的平台级项目正是用Golang实现的,而且相比其他的项目,它更依赖Golang,这一方面是因为Golang和谷歌之间的紧密关系,另一方面是因为项目在写和开发的过程中,谷歌工程师引入了很多独有的设计模式在里面,这也是我们要谈的内容。 和其他的项目不一样,很多项目说采用Golang的原因大多都是Golang的开发很方便,性能很好,或者并发编程很优秀。但对Kubernetes这样的项目来说,这些都不算是主要的理由。毕竟谷歌Borg项目是c++写的
  • How to use NuSMV to witness the man-in-the-middle attack (Needham-Schroeder protocol)?
    I have the following simplified public-key Needham-Schroeder protocol: A → B: {Na, A} Kb B → A: {Na, Nb} Ka A → B: {Nb} Kb where Na, Nb are the nonces of A, B, and Ka, Kb are the public keys of A, B respectively. Messages encrypted by a party’s public key can only be decrypted by the party. At Step (1), A initiates the protocol by sending a nonce and its identity (encrypted by B’s public key) to B. Using its private key, B deciphers the message and gets A’s identity. At Step (2), B sends A’s and its nonces (encrypted by A’s public key) back to A. Using its private key, A decodes the message
  • 在 OSX 上运行 NuSMV(Running NuSMV on OSX)
    问题 我已经使用提供的自述文件安装了 NuSMV,但是当我尝试使用 NuSMV 命令时,我收到以下消息:-bash: NuSMV: command not found 互联网上关于此的信息不多,所以我很感激任何帮助 回答1 转到我的主目录,并创建一个新的 bash 配置文件并使用 NuSMV 可执行文件附加 bin 目录使其工作正常。 回答2 如何让它在 MacOSX 上运行 到这个链接:http://nusmv.fbk.eu/ 点击 NuSMV 2.6.0 出来了! 选择:NuSMV 二进制图像 填写详细信息并注册:您将能够下载一个 zip 文件,将其解压缩并将其复制到您想要的任何位置。 现在我们需要设置路径。 打开终端并执行如下操作:将目录 /opt/nusmv-XYZ/bin 添加到您的命令搜索 PATH 环境变量中。 例如对于 bash shell: % 导出 PATH=${PATH}:/opt/nusmv-XYZ/bin 设置 NUSMV_LIBRARY_PATH 环境变量。 例如对于 bash shell: % 导出 NUSMV_LIBRARY_PATH=/opt/nusmv-XYZ/share/nusmv 现在您已准备好运行并享受 NuSMV。 % NuSMV -int # 运行交互模式
  • GRADS软件初步学习
    因为老师要求,只能学这个奇奇怪怪的东西了,希望以后能用到。 总览:这个小众的供气象工作人员画图的软件是怎么运作的呢? 数据处理(文件是不是GrADS能接受的格式,不行的话就要通过Fortran软件来转换文件格式)–》建立数据描述文件(有的时候直接就有,有时需要手写,我们不能直接使用数据文件,要通过数据描述文件来间接使用数据文件)–》输入GrADS命令或者建立批处理文件完成画图–》看图+存图 **1.格点数据和站点数据:**格点数据是什么呢?我们可以通过经度,纬度,高度在地球上确定一个位置,我们可以将这个位置视作一个格点,而一个格点上又有相应的数据,一些物理变量和时次变化。 此时如果固定了时间和高度,那么所有水平网格点就构成了一个二维网格数据片,每个数据片就是一个数据记录。最后这些二维数据片又组成了实际上的大数组(包含了所有的时空及物理量信息)。 2.数据描述文件: 我们知道了数据描述文件(.ctl)是必须有的,其实这是我们用记事本等编辑器写成的,写成之后文件名后缀用.ctl,保存类型为所有文件就可以了。写成之后如何使用呢? open D:\GrADS\DATA\model.ctl 打开之后就可以用其他命令对数据文件model.grd进行绘图和处理了。 那么现在还有一个主要问题,数据描述文件要怎么写呢? 下面是个例子 * this is an example to
  • 对于机架应用程序,如何让乘客独立提供 .erb 文件的输出而不是发送 .erb 文件本身?(For a rack app, how do I make passenger-standalone serve the output of .erb files rather of sending the .erb file itself?)
    问题 我有一个简单的config.ru rack 应用程序,我只需要和运行rack-server-pages就可以快速方便地提供动态页面。 此config.ru应用程序由 phusion 乘客独立(内部使用 nginx)提供服务。 .erb文件被正确处理和提供,除非我明确地将 .erb 扩展名添加到 URL(对于 .erb 文件)。 在这种情况下,服务器将向我发送 .erb 文件以供下载,而不是其输出。 显然,我想避免这种情况。 为了更清楚: 服务器上的文件名为somefile.erb 这有效: www.domain.com/somefile 这会发送 .erb 文件以供下载☹: www.domain.com/somefile.erb 我怎样才能解决这个问题? 这是我应该在应用程序级别(机架服务器页面)还是在 Web 服务器级别(nginx 配置)管理的问题? 在这两种情况下,我都需要一些帮助...... 更新 2:我认为这个 rack-server-pages 文件可能是相关的......但这只是一个疯狂的猜测,我不知道要改变什么...... 更新 1:粘贴乘客独立的 Nginx 配置文件。 Passenger-standalone内部使用 Nginx,但与/etc/nginx/nginx.conf的系统范围 Nginx 具有不同的设置。 乘客独立 Nginx
  • 在 Mac 上运行 NuSMV(Running NuSMV on Mac)
    问题 我下载了适用于 mac 的 NuSMV 源代码并开始使用自述文件进行安装。 但是,有一个步骤要求我在运行时使用“cmake..”进行构建,但出现问题源目录似乎不包含 CMakeLists.txt。 请问有什么帮助吗? 回答1 NuSMV二进制文件当然不需要编译,所以我推断你下载了NuSMV的源代码包。 该文件CmakeLists.txt载于..../NuSMV-<version>/NuSMV 。 再次检查您是否在这样的路径中创建了build目录[如README.txt文件要求您做的那样] ,或者只需将cmake <path>命令的参数设置为正确指向路径..../NuSMV-<version>/NuSMV 。
  • Coq 可以(轻松)用作模型检查器吗?(Can Coq be used (easily) as a model checker?)
    问题 正如标题所说,Coq 可以用作模型检查器吗? 我可以将模型检查与 Coq 证明混合使用吗? 这是常态吗? 谷歌谈论“微积分”,有没有人有这方面的经验或类似的经验? 是否建议以这种方式使用 Coq,或者我应该寻找其他工具? 回答1 像 Coq 这样的证明助手将验证您的证明是可靠的,并且您提出的任何定理都可以(或不能)使用公理和先前证明的结果推导出来。 它还将在提出证明步骤方面为您提供支持,以减少您为完成证明而必须付出的努力。 相比之下,模型检查器象征性地枚举规范的状态空间并确定是否违反了任何验证条件。 在这种情况下,它将提供错误跟踪,显示状态更改的顺序将触发违规。 这些通常具有非常不同的后端处理要求,但是,虽然它们可以组合成一个工具,但 Coq 证明器似乎没有这样做。 动作时间逻辑 (TLA+) 规范语言以及配套的 TLA+ 证明系统 (TLAPS) 由 Leslie Lamport 开发,用于推理大型正式规范。 它已使用 PlusCal 算法语言进行了扩展,该语言支持对转换为 TLA+ 表示的算法进行模型检查。 µ 演算是一种符号,用作许多形式方法方法的低级基础。 您还应该查看布尔可满足性问题以获得更强力的方法。 定理证明者的设计通常更复杂,并使用传统的专家系统/人工智能概念以及专家定义的证明规则库,以提供履行证明义务所需的支持。 作为证明工具的另一个示例,您可以查看
  • Redis IO多路复用技术及epoll实现原理
    10、Redis IO多路复用技术以及epoll实现原理 Redis是一个单线程的但性能是非常好的内存数据库,主要用来作为缓存系统。Redis采用网络IO多路复用技术来保证在多连接的时候,系统吞吐量高。 10.1 为什么Redis要使用IO多路复用 首先,Redis是跑在单线程中的,所有的操作都是顺序线性执行的,但是由于读写操作等待用户输入或者输出都是阻塞的,所以I/O操作往往不能直接返回,这会导致某一文件的I/O阻塞导致整个进程无法为客户服务,而I/O多路复用模型就是为了解决这个问题而出现的。 select、poll、epoll都是IO多路复用的模型。I/O多路复用就是通过一种机制,可以监视多个文件描述符,一旦某个描述符就绪,能够通知应用程序进行相应操作。 Redis的I/O模型使用的就是epoll,不过它也提供了select和kqueue的实现,默认采用epoll。 那么epoll到底什么东西?我们一起来看看。 10.2 epoll实现机制 10.2.1 场景举例 设想一个如下场景: 有100W个客户端同时与一个服务器保持着TCP连接。而每一时刻只有几百上千个TCP连接是活跃着的(事实上大部分场景都是这样的情况)。如何实现这样的高并发? 在select/poll时代,服务器进程每次都要把100W个连接告诉操作系统(从用户态复制句柄数据结构到内核态)
  • Running NuSMV on OSX
    I have installed NuSMV using the readme provided, however when I try to use the NuSMV command, I get the following message: -bash: NuSMV: command not found There isn't much information on the internet about this, so I'd appreciate any help
  • 如何让我的 Selenium 测试不那么脆弱?(How can I make my Selenium tests less brittle?)
    问题 我们使用 Selenium 来测试我们的 ASP.NET 应用程序的 UI 层。 许多测试用例测试跨越多个页面的较长流程。 我发现测试非常脆弱,不仅被实际更改页面的代码更改破坏,还被无害的重构破坏,例如重命名控件(因为我需要将控件的 clientID 传递给 Selenium 的 Click 方法等)或替换带有中继器的网格视图。 结果,我发现自己在“浪费”时间更新测试用例中的字符串值以修复损坏的测试。 有没有办法编写更易于维护的 Selenium 测试? 或者更好的 Web UI 测试工具? 编辑补充:一般第一稿是通过在IDE中记录一个测试来创建的。 (这第一步可能由 QA 人员执行。)然后我重构生成的 C# 代码(提取常量、提取重复代码的方法、可能用不同的数据重复测试用例等)。 但是每个测试用例的一般代码流仍然与最初生成的代码相当接近。 回答1 我发现 PageObject 模式非常有用。 http://code.google.com/p/webdriver/wiki/PageObjects 更多信息: - Selenium 的意义是什么? - 硒批判 也许一个好的开始方法是逐步重构您的测试用例。 我使用与您拥有 selenium + c# 相同的场景 这是我的代码的样子: 测试方法看起来像这样 [TestMethod] public void
  • Error Detection And Correction (EDAC)
    COPIED FROM: http://fibrevillage.com/sysadmin/243-edac-error-detection-and-correction https://01.org/linuxgraphics/gfx-docs/drm/driver-api/edac.html 1. Error Detection And Correction (EDAC) Devices Main Concepts used at the EDAC subsystem There are several things to be aware of that aren't at all obvious, like sockets, *socket sets, banks, rows, chip-select rows, channels, etc... These are some of the many terms that are thrown about that don't always mean what people think they mean (Inconceivable!). In the interest of creating a common ground for discussion, terms and their definitions will
  • ASP.NET 2.5前缀ctl00和ASP.NET 4不前缀ctl00(ASP.NET 2.5 prefixing ctl00 and ASP.NET 4 not prefixing ctl00)
    问题 有谁知道为什么ASP.NET 4在ASP控件上删除了ctl00前缀? 有没有我错过的设置? 回答1 在ASP.NET 4.0中,他们引入了对更简洁的HTML语法的支持。 您可以在Scott Gu的博客上了解有关它的信息。 如果您希望使用经典的客户端ID模型,则可以调整web.config: <configuration> <system.web> <pages controlRenderingCompatibilityVersion="3.5" /> 这将使您的应用程序升级更加容易。 您可以使用Control.ClientIDMode属性(也可以在Web配置中设置)针对每个控件(和每个页面)更改此设置: <configuration> <system.web> <pages clientIDMode="AutoID|Predictable|Static|Inherit" /> AutoID使用经典的ASP.NET 2.0模型呈现控件。 回答2 据我记得,由ASP.NET决定使用哪个前缀。 在具有硬编码id值的控件上进行引用是一种不好的做法。 您应该使用ClientId属性,该属性将始终为您生成正确的ID: <td class="tmarg10" style="width: 150px"> <label for="<%=txtName.ClientID %>"> Name of