Transition semantics for QCHR implemented in swipl

• Some tools
• Main program

Small examples that test the structural rules of the transition system:

• Example 1 :
  exists_0 {It, 0, 2} exists_1
  exists_1 {It, 10, 12} exists_2
  exists_2 {It, 101, 102} true
• Example 2 :
  exists_0 {It, 0, 2} exists_1, exists_2
  exists_1 {It, 10, 12} exists_11, exists_12
  exists_11 {It, 110, 112} true
  exists_12 {It, 120, 122} true
  exists_2 {It, 20, 22} exists_21, exists_22
  exists_21 {It, 210, 212} true
  exists_22 {It, 220, 222} true
• Example 3 :
  exists_0 {It, 0, 2} c_0(It), exists_1(It), c_0(It)
  exists_1(It_0) {It, 10, 12} c_1(It_0, It_1), exists_2(It_0,It), c_1(It_0, It_1)
  exists_2(It_0,It_1) {It, 100, 102} c_2(It_0,It_1,It)
  c_0(_) <=> c
  c_1(_,_) <=> c
  c_2(_,_,_) <=> c
  c <=> true
• Example 4 :
  exists_0 {It, 0, 2} c_0(It)
  c_0(0) <=> false
  c_0(1) <=> false
  c_0(2) <=> c
  c <=> true
• Example 5 :
  exists_0 {It, 0, 2} exists_1(It)
  exists_1(It_0) {It, 10, 12} exists_2(It_0,It)
  exists_2(It_0,It_1) {It, 100, 102} c_1(It_0,It_1,It)
  c_1(It_0,It_1,It) <=> c_2(It_0,It_1,It)
  c_2(0,_,_) <=> false
  c_2(1,_,_) <=> false
  c_2(2,10,_) <=> false
  c_2(2,11,_) <=> false
  c_2(2,12,100) <=> false
  c_2(2,12,102) <=> false
  c_2(2,12,101) <=> true
  
• Example 6 :
  exists_0 {It, 0, 2} exists_1(It)
  exists_1(It_0) {It, 10, 12} exists_2(It_0,It)
  exists_2(It_0,It_1) {It, 100, 102} c_1(It_0,It_1,It)
  c_1(It_0,It_1,It) <=> c_2(It_0,It_1,It)
  c_2(_,_,_) <=> false
  
• Example 7 :
  univ_0 {It, 0, 2} univ_1
  univ_1 {It, 10, 12} true
  
• Example 8 :
  univ_0 {It, 0, 2} univ_1
  univ_1 {It, 10, 12} univ_2
  univ_2 {It, 101, 102} true
  
• Example 9 :
  univ_0 {It, 0, 2} true
  univ_1 {It, 10, 12} true
  
• Example 10 :
  univ_0 {It, 0, 2} c_0(It), univ_1(It), c_0(It)
  univ_1(It_0) {It, 10, 12} c_1(It_0, It_1), univ_2(It_0,It), c_1(It_0, It_1)
  univ_2(It_0,It_1) {It, 100, 102} c_2(It_0,It_1,It)
  c_0(_) <=> c
  c_1(_,_) <=> c
  c_2(_,_,_) <=> c
  c <=> true
• Example 11 :
  univ_0 {It, 0, 2} univ_1, univ_2
  univ_1 {It, 10, 12} univ_11, univ_12
  univ_11 {It, 110, 112} true
  univ_12 {It, 120, 122} true
  univ_2 {It, 20, 22} univ_21, univ_22
  univ_21 {It, 210, 212} true
  univ_22 {It, 220, 222} true
• Example 12 :
  exists_0 {It_0, 0, 1} univ_1(It_0)
  univ_1(It_0) {It_1, 10, 11} exists_2(It_0,It_1)
  exists_2(It_0,It_1) {It_2, 100, 101} univ_3(It_0,It_1,It_2)
  univ_3(It_0,It_1,It_2) {It_3, 1000, 1001} c_1(It_0,It_1,It_2, It_3)
  c_1(It_0,It_1,It_2, It) <=> c_2(It_0,It_1,It_2, It)
  c_2(0,It_1,It_2,1001) <=> true
  c_2(0,It_1,It_2,_) <=> (It_1 = 11 & It_2 = 100) | true
  c_2(0,It_1,It_2,_) <=> !((It_1 = 11 & It_2 = 100)) | false
  c_2(1,_It_1,It_2,_)] <=> It_2 = 101 | true
  c_2(1,_It_1,It_2,_)] <=> !(It_2 = 101) | false
  
• Example 13 :
  univ_0 {It, 0, 2} univ_1(It)
  univ_1(It_0) {It, 10, 12} univ_2(It_0,It)
  univ_2(It_0,It_1) {It, 100, 102} c_1(It_0,It_1,It)
  c_1(It_0,It_1,It) <=> c_2(It_0,It_1,It)
  c_2(2,10,100) <=> false
  c_2(_,_,_) <=> true
  
• Example 14 :
  exists_0 {It_0, 0, 2} c, univ_1(It_0), c
  univ_1(It_0) {It_1, 10, 12} c, exists_2(It_0,It_1), c
  exists_2(It_0,It_1) {It_2, 100, 102} c
  c <=> true
  
• Example 15 :
  exists_0 {It_0, 0, 2} univ_1(It_0)
  univ_1(It_0) {It_1, 10, 12} exists_2(It_0,It_1)
  exists_2(It_0,It_1) {It_2, 100, 102} c_1(It_0,It_1,It_2)
  c_1(It_0,It_1,It) <=> c_2(It_0,It_1,It)
  c_2(0,It_1,It_2) <=> (It_1 = 12 & It_2 = 102) | true
  c_2(0,It_1,It_2) <=> !(It_1 = 12 & It_2 = 102) | false
  c_2(1,It_1,It_2) <=> (It_1 = 11 & It_2 = 101) | true
  c_2(1,It_1,It_2) <=> !(It_1 = 11 & It_2 = 101) | false
  c_2(2,_It_1,It_2) <=> It_2 = 101 | true
  c_2(2,_It_1,It_2) <=> !(It_2 = 101) | false
  
• Example 16 :
  exists_0 {It_0, 0, 0} univ_1(It_0)
  univ_1(It_0) {It_1, 10, 10} exists_2(It_0,It_1)
  exists_2(It_0,It_1) {It_2, 100, 102} univ_3(It_0,It_1,It_2)
  univ_3(It_0,It_1,It_2) {It_3, 1000, 1001} c_1(It_2)
  c_1(It) <=> c_2(It)
  c_2(100) <=> false
  c_2(101) <=> true
  
• Example 17 :
  exists_0 {_, 0, 0} c, univ_1, c
  univ_1 {_, 0, 0} c, exists_2, c
  exists_2 {It_0, 0, 1} c, univ_2(It_0), c
  univ_2(It_0) {It_1, 10, 11} c, c_1(It_0,It_1), c
  c_1(It_0,It_1) <=> c, c_2(It_0,It_1), c
  c_2(0,10) <=> true
  c_2(0,11) <=> false
  c_2(1,10) <=> true
  c_2(1,11) <=> true
  c <=> true