source: cegar_dev/cegar/abstract_model/machine_concret.ctl

Last change on this file was 4, checked in by syed, 14 years ago

input files added
File size: 1.0 KB
Line 
1# Phi_1 :
2(r_i1 = 0)  + AF (o1 = 1);
3# Expected result : formula passed
4#---------------------------------------------------------
5# Phi_2 :
6(r_i1 = 0)  + AF (o2 = 1);
7# Expected result : formula passed
8#---------------------------------------------------------
9# Propriéte globale :
10(o1 = 0)  + AF (o2 = 1);
11# Expected result : formula passed
12#---------------------------------------------------------
13A((o1 = 0) U((o1 = 1) * AF(o2 = 1)));
14# Expected result : formula passed
15#---------------------------------------------------------
16#A((o1 = 0) U((o1 = 1) * AG(o2 = 1)));
17# Expected result : formula passed
18#---------------------------------------------------------
19#(r_i1 = 0)  + AF (((o1=1) *( o2 = 1)));
20# Expected result : formula passed
21#---------------------------------------------------------
22#(r_i1 = 0) + (AF(o1 = 1) * AF (o2 = 1));
23# Expected result : formula passed
24#---------------------------------------------------------
25#AG (o2 = 0);
26# Expected result : formula passed (Counter-example test)
27#---------------------------------------------------------
Note: See TracBrowser for help on using the repository browser.