source: cegar_dev/cegar/concrete_model/machine_concret.ctl @ 28

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

input files added
File size: 935 bytes
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(r_i1 = 0)  + AF (((o1=1) *( o2 = 1)));
17# Expected result : formula passed
18#---------------------------------------------------------
19(r_i1 = 0) + (AF(o1 = 1) * AF (o2 = 1));
20# Expected result : formula passed
21#---------------------------------------------------------
22AG (o2 = 0);
23# Expected result : formula failed (Counter-example test)
24#---------------------------------------------------------
Note: See TracBrowser for help on using the repository browser.