1.应用于自动售卖机系统的基于模型检测的反例精化系统，其特征在于，包括最短路径构建模块、最短路径事件处理模块、事件顺序检测模块和非最短路径事件处理模块；

其中，所述最短路径构建模块负责从模型检测产生的反例集合中提取并构建自动售卖机系统模型的最短路径集合和非最短路径集合；

所述最短路径事件处理模块负责处理最短路径集合以及非最短路径集合，包括：检测最短路径集合中包含的每一条路径是否为非最短路径集合中任意一条路径的真子集，并且最短路径集合中包含的每一条路径中事件是否与非最短路径集合中任意一条路径中事件顺序一致；

所述事件顺序检测模块包括一个输入端口和一个输出端口，通过输入端口输入需要检测的路径集合，输出端口输出已标记过顺序相关的需要检测的路径集合，以对需要检测的路径集合中包含的事件标注其是否顺序相关；

所述非最短路径事件处理模块负责对非最短路径集合进行处理，包括：将非最短路径集合与最短路径集合中路径进行比较，并标记是否顺序相关，将符合条件的非最短路径加入到最短路径集合中，并对最短路径集合以及非最短路径集合进行更新。

2.根据权利要求1所述的系统，其特征在于，系统执行如下步骤：

步骤1，所述最短路径构建模块对自动售卖机系统建立系统模型，得到最短路径集合Pd和非最短路径集合P′d；

步骤2，所述最短路径事件处理模块对最短路径集合Pd和非最短路径集合P′d分别进行处理：所述最短路径事件处理模块依次从最短路径集合Pd取出其中包含的每条路径用于比较，设定取出的第k条路径表示为 依次为最短路径集合Pd中的路径顺序编号，k表示取出的路径在最短路径集合Pd中的编号，为正整数，取出时从编号k＝1的最短路径开始，顺序递增取出，当取出一条路径时，同时将非最短路径集合P′d的所有路径依次取出与其进行比较，设从非最短路径集合P′d中取出比较的第n条路径为L'n，依次为最短路径集合Pd中的路径顺序编号，设n为从非最短路径集合P′d取出比较的路径的编号，取出时从编号n＝1的最短路径开始，顺序递增取出；比较路径 与路径L'n，判断路径 是否为路径L'n的子集，并且路径L'n中事件是否与路径 中事件顺序一致；其中，k的值最大为最短路径集合Pd中包含的路径条数，n的值最大为非最短路径集合P′d中包含的路径条数；

步骤3，所述事件顺序检测模块通过输入端口输入需要检测的路径集合，需要检测的路径集合为最短路径集合Pd，将需要检测的路径集合中所有路径依次一一提取，设需要检测的路径集合中当前提取的路径为路径L1，先设定路径L1中包含的所有事件两两之间为顺序相关的，随后，将最短路径集合Pd中除了路径L1之外的路径分别一一提取，一一与路径L1进行比较，以判断路径L1中包含的事件之间是否顺序相关；

步骤4，所述非最短路径事件处理模块对非最短路径集合P′d进行检测。

3.根据权利要求2所述的系统，其特征在于，步骤1包括：

步骤1-1，最短路径构建模块对自动售卖机系统建立系统模型，将系统模型中所有路径提取出来，得到路径集合P；

步骤1-2，最短路径构建模块在系统模型之上进行模型检测，将路径集合P分为两类：反例集合P1和非反例集合P2，即P＝P1∪P2；其中反例集合P1包含所有经由模型检测产生的反例路径，非反例集合P2则包含路径集合P中除了反例路径之外的所有其他路径；

步骤1-3，最短路径构建模块对反例集合P1中所有路径进行一一检测，检测其是否为最短路径，并且将反例集合P1中包含的所有最短路径加入到最短路径集合Pd中，将反例集合P1中除了最短路径之外的所有其他路径加入到非最短路径集合P′d中，即P1＝Pd∪P′d。

4.根据权利要求3所述的系统，其特征在于，步骤1-3包括如下步骤：

步骤1-3-1，初始时最短路径集合Pd为空集，一一检测反例集合P1中的路径，设反例集合P1P1中正在检测的路径为当前检测路径，将反例集合P1中所述当前检测路径都与反例集合P1中除了当前检测路径之外的其他路径一一比较，检测当前检测路径是否包含反例集合P1中除了当前检测路径之外的任意一条路径，或者当前检测路径是否与反例集合P1中除了当前检测路径之外的任意一条路径完全一样，如果满足任一个条件，则当前检测路径不为最短路径，否则将当前检测路径加入到最短路径集合Pd中，将最短路径集合Pd中的路径一一设为当前检测路径进行检测，直到最短路径集合Pd中所有路径都经过检测。

5.根据权利要求4所述的系统，其特征在于，步骤1-3-1中，检测当前检测路径是否包含反例集合P1中除了当前检测路径之外的任意一条路径，或者当前检测路径是否与反例集合P1中除了当前检测路径之外的任意一条路径完全一样的过程为：步骤1-3-1-1，最短路径构建模块将反例集合P1中除了当前检测路径之外的每一条路径中包含的事件提取，提取到一个事件集合中，将提取的事件集合表示为Event_P(i)，i为提取的路径在反例集合P1中的编号，反例集合P1中所有路径都从1开始顺序编号，编号为正整数，且大于等于1，将当前检测路径中包含的事件提取，提取的事件集合表示为Event_P(j)，j为当前检测路径在反例集合P1中路径的编号，为正整数，并且j≠i；反例集合P1中路径的编号由用户按顺序编号，其中，Event_P表示事件集合，i，j为变量,i和j的值不断变化，由步骤

1-3-1-2检测的过程决定，比较的是路径编号；

步骤1-3-1-2，对当前检测路径都进行判断过程，从i＝1开始，j≠i，依次进行如下判断：

如果 表示事件集合Event_P(i)中的事件都在事件集合Event_P

(j)中，并且Event_P(i)包含的事件个数小于Event_P(j)包含的事件个数，则判断当前检测路径包含了反例集合P1中除了当前检测路径之外的任意一条路径；

如果Event_P(i)＝Event_P(j)，表示事件集合Event_P(j)与事件集合Event_P(i)为同一个事件集合，这两个事件集合相等，并且Event_P(i)包含的事件个数等于Event_P(j)包含的事件个数，则判断当前检测路径等于反例集合P1中除了当前检测路径之外的任意一条路径；

如果当前检测路径包含了反例集合P1中除了当前检测路径之外的任意一条路径，或当前检测路径又等于反例集合P1中除了当前检测路径之外的任意一条路径，将当前检测路径作为非最短路径加入非最短路径集合P′d中；

步骤1-3-1-3，在步骤1-3-1-2中的判断完毕后，如果当前检测路径已作为非最短路径加入到非最短路径集合P′d中，则进行反例集合P1中的下一条路径判断，将i更新为i+1，当前检测路径为反例集合P1中编号为i的路径，如果i小于等于反例集合P1中路径的个数，继续进行步骤1-3-1-2判断过程；

当i大于反例集合P1中路径的个数，停止步骤1-3-1-2的判断过程，若此时停止判断过程时，当前检测路径不为非最短路径，则当前检测路径再作为最短路径加入到最短路径集合Pd中；取反例集合P1中下一条路径作为当前检测路径，重复步骤1-3-1-1，直到反例集合P1中所有路径都经过判断，得到最短路径集合Pd和非最短路径集合P′d。

6.根据权利要求5所述的系统，其特征在于，步骤2具体包括如下步骤：

步骤2-1，所述最短路径事件处理模块判断路径 中包含事件的数量是否小于等于路径L'n中包含的事件数量，判断的方法为：分别对路径 路径L'n中包含的事件进行计数，比较两者的数量大小，当路径 中包含事件的数量小于等于路径L'n中包含的事件数量，再执行步骤2-2，并且分别对路径 路径L'n中包含的事件进行编号，对路径 中事件编号的顺序为按照路径 中事件有序序列中事件先后顺序发生的顺序分别编号，则路径 中m个事件按时间发生先后顺序依次记为 m为路径 中包含的事件个数；

对路径L'n中事件编号的顺序为按照路径L'n中事件有序序列中事件先后顺序发生的顺序分别编号，则路径L'n中l个事件按时间发生先后顺序依次记为 l为路径L'n中包含的事件个数；其中，m≤l；

步骤2-2，最短路径事件处理模块从路径 中的事件有序序列中先后顺序提取其中的事件，即按顺序提取 表示的事件，依次在路径L'n中寻找与路径 中

包含的事件相同的事件，如果能在路径L'n中寻找到所有与路径 中包含的事件相同的事件，再进行提取，提取的顺序为按照事件 的顺序提取相应的事件，提

取其代表的事件在路径L'n中的编号，按照提取的顺序组成编号序列，把编号序列的下标提取，组成下标序列，下标序列中所有下标必须满足升序排列的条件，则路径 为路径L'n的子集，并且路径L'n中事件与路径 中事件顺序一致，继续步骤2-3，如果不能在路径L'n中寻找到所有与路径 中包含的事件相同的事件，则直接执行步骤3；

步骤2-3，如果路径 为路径L'n的子集，并且路径L'n中事件与路径 中事件顺序一致，所述最短路径事件处理模块将路径 中包含的事件提取到事件有序集合OE1中，同时将路径L'n中包含事件提取到事件有序集合OE2中，将事件有序集合OE2与一个布尔事件集合Bn对应，布尔事件集合Bn包含l个布尔事件，第一个至第l个布尔事件依次记为 布尔事件 只有true、false两个值，用以表示路径L'n中包含的对应事件是否被包含在路径 中；布尔事件 的所有值初始被设置为真值true，布尔事件 分别与路径L'n中的事件 一一对应，即第一个布尔事件 与第一个事件 相对应，当布尔事件 的值为true，表示路径L'n中包含的第一个事件 被包含在路径 中，当布尔事件 的值为false，表示路径L'n中包含的第一个事件 不被包含在路径 中；依次类推，第l个布尔事件 与第l个事件 相对应，当布尔事件 的值为true，表示路径L'n中包含的第l个事件 被包含在路径 中，当布尔事件 的值为false，表示路径L'n中包含的第l个事件 不被包含在路径 中，即布尔事件与路径L'n中被编号的事件的下标相等，则两者存在对应关系；为将在事件有序集合OE2而不在事件有序集合OE1中的事件对应的布尔事件的值设置为假值false，与被设置为false的布尔事件下标相同的在路径L'n中的事件取反，路径L'n中包含的事件在事件有序集合OE2中而不在事件有序集合OE1中的事件取反，得到的路径命名为 并建立路径对 其中，事件有序集合为事件按其发生时间先后顺序排列的事件集合。

7.根据权利要求6所述的系统，其特征在于，步骤3包括如下步骤：

步骤3-1，所述事件顺序检测模块从需要检测的路径集合即所述最短路径集合Pd中一一提取路径进行比较，设当前提取的路径为L1，接着，从所述最短路径集合Pd中一一提取除了路径L1以外的路径以进行比较，设所述最短路径集合Pd中提取的与路径L1进行比较的路径为L2，根据每次提取比较的路径不同，L2代表的路径也不同，将路径L1中包含的事件提取到事件有序集合OE3，同时将路径L2中包含的事件提取到事件有序集合OE4，在事件有序集合OE3、事件有序集合OE4中的事件按照事件发生的时间先后顺序排列，对比事件有序集合OE3、事件有序集合OE4中的事件是否完全相等并且排列的顺序也完全一致，如果是，则路径L1、路径L2为同一条路径，将路径L2从最短路径集合Pd中去除；

步骤3-2，比较事件有序集合OE3与事件有序集合OE4中包含的事件，把相同的事件分别提取到事件有序集合OE8以及事件有序集合OE9中，其中，事件有序集合OE8中事件排列的顺序与事件有序集合OE3中相同事件排列的顺序一致，事件有序集合OE9中事件排列的顺序与事件有序集合OE4中相同事件排列的顺序一致；从事件有序集合OE8提取所有事件有序对，为每一个事件有序对配对一个顺序标签，顺序标签为一个布尔变量，当顺序标签的值为真值true，表示其配对的事件有序对为顺序相关的，当顺序标签的值为假值false，表示其配对的事件有序对不是顺序相关的；初始时，置所有的顺序标签为真值true，具体过程如下：所述事件有序对包含事件一、事件二，事件有序对被表示为，表示事件一发生在事件二之前，其中事件一被表示为Event1，事件二被表示为Event2；Event1、Event2同时表示事件变量，用于代表不同的事件；从事件有序集合OE8中按照其中排列的先后顺序依次提取一个事件到Event1，提取后再从事件有序集合OE8中排列在事件Event1后的事件中依次提取一个事件到Event2，完成一个事件有序对后，从事件有序集合OE9按照事件排列先后的顺序寻找与Event2代表的事件相同的事件，其后，在事件有序集合OE9中寻找排列Event2代表事件相同的事件，如果找到后，并且Event1代表相同的事件在事件有序集合OE9中排列在与Event2代表事件相同的事件之后，如果相等，置事件有序对配对的顺序标签的值为假值false；

步骤3-3，对需要检测的路径集合中所有路径都进行步骤3-1～步骤3-2，直到所有路径都被检测是否顺序相关。

8.根据权利要求7所述的系统，其特征在于，步骤4包括如下步骤：

步骤4-1，非最短路径事件处理模块从非最短路径集合P′d中一一提取路径，设置当前从非最短路径集合P′d中提取的路径为L3，L3代表当前提取的路径，其代表的路径是不断变化的，并设置计数器C，计数器C的初始值为0，将计数器C的值设置为初始值，将提取的路径与最短路径集合Pd中所有路径一一比较，比较是否包含最短路径集合Pd中任一条路径，设定从最短路径集合Pd提取的用于当前比较的路径为L4，L4代表比较的路径，其代表的路径是不断变化的，检测路径L3中包含的事件个数是否多于路径L4中包含的事件个数，如果是，将路径L4中包含的事件提取到事件有序集合OE5中，将路径L3中包含的事件提取到事件有序集合OE6，从事件有序集合OE5中一一提取出来单个事件，分别一一检测提取出的单个事件是否被包含在事件有序集合OE6中，如果事件有序集合OE5中所有事件都被包含在事件有序集合OE6中，使用计数器C加一，继续重复与最短路径集合Pd中下一条路径进行比较，比较是否包含最短路径集合Pd中下一条路径，直到最短路径集合Pd中所有路径都经过比较；当下一轮比较时，L3、L4分别代表下一条从非最短路径集合P′d中取出的路径、从最短路径集合Pd中取出的路径；

步骤4-2，当计数器C的值小于二时，直接从非最短路径集合P′d提取下一条路径，作为路径L3，重新开始步骤4-1；当计数器C的值大于等于二时，再一一从非最短路径集合P′d中提取路径，一一检测非最短路径集合P′d中除了路径L3的其他任意一条路径是否为路径L3的子集，设置从非最短路径集合P′d中提取除了路径L3的其他一条路径为L5，检测路径L3中包含的事件个数是否多于或者等于路径L5中包含的事件个数，如果是，将路径L5中包含的事件提取到事件有序集合OE7中，将路径L3中包含的事件提取到事件有序集合OE6，从事件有序集合OE7中一一提取出来事件，分别一一检测从事件有序集合OE7中提取出的事件是否被包含在事件有序集合OE6中，如果事件有序集合OE7中所有事件都被包含在事件有序集合OE6中，中断执行步骤4-3、步骤4-4，当所有的非最短路径集合P′d中的路径都已经被提取出来与路径L3比较过，并且步骤4-3、步骤4-4没有被中断，即路径L3不包含除了本身以外其他非最短路径，继续执行步骤4-3；路径L5是从非最短路径集合P′d中提取的一一进行比较的路径；

步骤4-3，非最短路径事件处理模块将路径L3输入到事件顺序检测模块的输入端口，此时需要检测的路径集合为仅包含路径L3一条路径的集合，即需要检测的路径集合只包含一条路径L3，重复步骤3的过程，将需要检测的路径集合中所有路径依次一一提取，设当前提取的路径为路径L1，此时路径L1等于路径L3，设定路径L3中包含的所有事件两两之间为顺序相关的，将最短路径集合Pd中的路径一一提取，一一与路径L3进行比较，以判断路径L3中包含的事件之间是否顺序相关，并对路径L3中所有事件的顺序相关性进行标号，判断路径L3中包含的事件之间是否顺序相关的过程与步骤3相同；

当非最短路径事件处理模块将路径L3经过步骤3的步骤处理完毕后，再查看路径L3是否经过步骤2的处理，即是否被建立路径对，如果路径L3被建立了路径对，撤销路径对，将路径L3从非最短路径集合P′d取出，加入到最短路径集合Pd中；

步骤4-4，非最短路径事件处理模块依次从非最短路径集合P′d一一提取路径，作为路径L3，重复步骤4-3，直到非最短路径集合P′d中所有路径都被提取处理完毕。

9.根据权利要求8所述的系统，其特征在于，步骤1中，所述自动售卖机系统为购买咖啡和啤酒的自动售卖机系统，购买咖啡和啤酒的自动售卖机在使用时，当投币后，能够选择购买咖啡或者啤酒，只有向自动售卖机内投入两枚硬币才能进行选择，如果硬币数量少会等待下一步的动作，如果没有动作退币并返回初始状态，如果继续投币则可进行选择购买咖啡或啤酒，建立购买咖啡和啤酒的自动售卖机系统模型的过程为：将系统执行的完整正确路线都列出来，即系统开始运行到终止的所有的正确执行路线，并将其使用事件有序序列进行表示，即正确执行路线中所有执行所发生的动作表示成事件，所有的正确执行路线的事件有序序列组合成了系统模型；

购买咖啡和啤酒的自动售卖机系统的工作模式为：投入硬币后，需要投入两枚硬币才能选择是咖啡还是啤酒，两枚硬币可以一起投入，也可以投入一枚后根据提示再进行投入，选择完毕后得到选择的咖啡或啤酒，最后系统重置回到最初状态；如果只投入一枚硬币，等待再投入一枚，如果再投入一枚可以进入上述一样的选择状态，选择咖啡还是啤酒，否则返回硬币，系统重置回到最初状态；

其中，用pay表示既是初始状态也是最终状态的状态，在此状态等待投入硬币，insert_one_coin表示投入一枚硬币的动作，coin not_enough表示硬币没有投入足够的状态，insert_two_coin表示投入两枚硬币的动作，select表示可以选择咖啡或啤酒的状态，select coffee表示选择咖啡的动作，select beer表示选择啤酒的动作，coffee表示选择了咖啡的状态，beer表示选择了啤酒的状态，get_coffee表示得到咖啡的动作，get_beer表示得到啤酒的动作，get coffee表示得到咖啡成功后转入的状态，get_beer表示得到啤酒成功后转入的状态，resetting表示对购买咖啡和啤酒的自动售卖机进行重置，not action表示在投了一枚硬币后没有进一步的动作，return_coin表示将硬币进行返回的动作，return coin表示将要将硬币返回而进入的状态；上述使用字母组以及下划线组合表示了系统的动作以及状态，系统的动作代表事件，在等待投入硬币pay状态后，能够进行选择投入一枚硬币insert_one_coin的动作后进入coin not enough状态，再选择投入一枚硬币insert_one_coin的动作，也能够选择直接insert_two_coin投入两枚硬币的动作，两种都进入select状态，select状态中能够选择selectcoffee的动作即选择咖啡，也能够选择selectbeer的动作即选择啤酒，选择完毕后得到用get beer、get coffee两个动作分别描述得到啤酒、得到咖啡的动作，各自分别进入get beer、get coffee这两个状态，能够选择resetting动作对系统进入重置再进入pay状态，同时，如果只投入一枚硬币，insert_one_coin的动作后进入coin not enough状态后，如果没有动作即not action的动作发生，则进行返回硬币return coin的动作后再对系统进入重置resetting的动作再进入pay状态，用箭头表示状态转换的方向即路线的方向，在箭头上使用字母描述动作，发生该动作后进入下一个状态，直到到达最终状态，对系统模型进行检查，直到所有正确执行路线都被描述在系统模型中，系统路径为从初始状态pay到最终状态pay状态的路径，路径中记录了经过的状态以及动作，路径包括：(1)

(2)

(3)

(4)

(5)

设定需要检测两条性质F(get beer)、EF(get beer)，前一条性质F(get beer)表示能够到达买到啤酒的状态，后一条性质EF(get beer)表示存在一条能够到达买到啤酒的状态；

所述系统一共五条路径，即编号为(1)到(5)的五条路径，形成路径集合P，其中编号(1)(3)(4)的路径被包含在反例集合P1中，编号(2)(5)的路径被包含在非反例集合P2中；

所述反例精化系统在应用于购买咖啡和啤酒的自动售卖机时执行如下步骤：

步骤a1，反例集合P1编号(1)(3)(4)的路径在反例集合P1中分别被编号为1、2、3，即在反例集合P1中编号(1)(3)(4)的路径分别编号为1、2、3；分别将路径编号1、2、3路径中事件提取到事件集合Event_P(1)、Event_P(2)、Event_P(3)中：Event_P(1)＝{insert_one_coin、insert_one_coin、select coffee、get_coffee、resetting}；

Event_P(2)＝{insert_one_coin、not action、resetting}；

Event_P(3)＝{insert_two_coin、select coffee、get_coffee、resetting}；

事件集合Event_P(1)、Event_P(2)、Event_P(3)不存在包含与被包含关系，因此，将反例集合P1中编号(1)(3)(4)的路径加入到最短路径集合Pd中，非最短路径集合P′d为空集；

步骤a2，在所述步骤2中，考虑的是最短路径集合Pd与非最短路径集合P′d中路径的关系、事件包含关系、事件顺序是否一致，在应用于购买咖啡和啤酒的自动售卖机时，非最短路径集合P′d为空集，因此步骤2的过程省略；

步骤a3，检测最短路径集合Pd，先提取路径L1，路径L1取在反例集合P1中路径编号为1的路径，路径L2取在反例集合P1中路径编号为2的路径，分别将其中包含的事件提取到事件有序集合OE3、事件有序集合OE4中：OE3＝OE4＝与事件集合Event_P(1)、Event_P(2)的区别在于事件有序集合中事件是顺序相关的，将其中包含的相同的事件提取到事件有序集合OE8，OE8＝，事件顺序与事件有序集合OE3中事件的顺序保持一致，另外将其中包含的相同的事件提取到事件有序集合OE9中，顺序与事件有序集合OE4中事件的顺序保持一致，OE9＝，两个事件有序集合OE3、事件有序集合OE9都只有两个事件，依次提取两个事件到事件有序对中，＝，即Event1＝insert_one_coin，Event2＝resetting，在事件有序集合OE9中与事件有序集合OE3事件顺序一致，在事件有序集合OE9与Event2相同的事件resetting排列在后，与Event1相同的事件insert_one_coin排列在前，因此，事件有序对顺序标签为true；

接着，再提取路径L1，路径L1取在反例集合P1中路径编号为1的路径，路径L2取在反例集合P1中路径编号为3的路径，分别将其中包含的事件提取到事件有序集合OE3、事件有序集合OE4中：事件有序集合OE3维持不变，OE4＝，将其中包含的相同的事件提取到事件有序集合OE8，OE8＝，依次按顺序提取两个事件到事件有序对＝，另外将其中包含的相同的事件提取到事件有序集合OE9中，OE9＝，顺序与事件有序集合OE4中事件的顺序保持一致，而OE9与OE8一致相同，该事件有序对的顺序标签仍然为true，另外提取事件有序对＝，经过分析提取的OE9与OE8一致相同，所以事件有序对的顺序标签仍然为true；

再提取路径L1，路径L1取在反例集合P1中路径编号为2的路径，路径L2取在反例集合P1中路径编号为3的路径，分别将其中包含的事件提取到事件有序集合OE3、事件有序集合OE4中：将其中包含的相同的事件提取到事件有序集合OE8＝OE9＝，只有一个事件，不存在事件有序对。