Change the structure of "main.sfp"

[herry13]

Example specification in "main.sfp"

// the desired state
vm1 isa VM {
    web isa Apache
    db isa Mysql {
        running is true
    }
}
vm1.web.running is true
// constraint at goal state
constraint goal {
    if vm1.web.running then vm1.db.running
}
constraint global {
}

Another example

// the desired state
foo isa Machine {
    address is "foo.domain"
    web isa Apache
    db isa Mysql
}
// mutation
foo.web.running is true
// a constraint
if foo.web.running then foo.db.running
// global constraint
global {
    if foo.web.running then foo.db.running
}

[herry13]

Example of configuration task after adding current state and schemas

//--- start of schemas ---//
schema VM
schema Apache {
    running is false
}
schema Mysql {
    running is false
}
//--- end if schemas ---//
//--- start of initial state ---//
initial {
    vm1 isa VM {
        web isa Apache {
            running is false
        }
        db isa Mysql {
            running is false
        }
    }
}
//--- end of initial state ---//
//--- start of goal ---//
vm1 isa VM {
    web isa Apache
    db isa Mysql {
        running is true
    }
}
vm1.web.running is true
constraint goal {
    if vm1.web.running then vm1.db.running
}
constraint global {
}
//--- end of goal

[herry13]

After compilation:

schemas:
[VM] = [schema [Object] []]
[Apache] = [schema [Object] []]
[Apache][2][running] = [var Bool false]
[Mysql] = [schema [Object] []]
[Mysql][2][running] = [var Bool false]

initial (domain: nested Hashtable):
[vm1] = [val [Object VM] []]
[vm1][2][web] = [val [Object Apache] []]
[vm1][2][web][2][running] = [var Bool false]
[vm1][2][db] = [val [Object Mysql] []]
[vm1][2][db][2][running] = [var Bool false]

initial (domain: single Hashtable):
[vm1] = [val [Object VM] []]
[vm1.web] = [val [Object Apache] []]
[vm1.web.running] = [var Bool false]
[vm1.db] = [val [Object Mysql] []]
[vm1.db.running] = [var Bool false]

goal (first-order logic formulae):
[and
    [= vm1.web.running true]
    [= vm1.db.running true]
    [imply [= vm1.web.running true] [= vm1.db.running true]]
]

global (first-order logic formulae):
[and true]

[herry13]

Content of main.sfp:

a isa Service
b isa Service {
    running is true
}
pc isa Client {
    refer either Service
    // this also can be written:
    // refer either (a, b)
}
global {
    pc.refer.running is true
}

Combining initial state, goal/global constraints, and schemas:

schema Service {
    running is false
}
schema Client {
    refer isref Service
}
a isa Service {
    running is true
}
b isa Service {
    running is false
}
pc isa Client {
    refer is a
}
goal {
    a.running is false
}
global {
    pc.refer.running is true
}

Compilation step-1:

// schemas (domain: nested Hashtable)
[Service] = [schema [Object] []]
[Service][2][running] = [var Bool false]
[Client] = [schema [Object] []]
[Client][2][running] = [var Service null]

// initial state (domain: nested Hashtable)
[a] = [val [Object Service] []]
[a][3][running] = [var Bool true]
[b] = [val [Object Service] []]
[b][3][running] = [var Bool false]
[pc] = [val [Object Client] []]
[pc][3][refer] = [var Service a]

// goal constraint (domain: array of first-order logic formulae)
[and
    [= a.running false]
]

// global constraint (domain: array of first-order logic formulae)
[and
    [= pc.refer.running true]
]

Compilation step-2:

// initial state (domain: Hashtable)
[a] = [val [Object Service] []]
[a.running] = [var Bool true]
[b] = [val [Object Service] []]
[b.running] = [var Bool false]
[pc] = [var [Object Client] []]
[pc.refer] = [var Service a]

// goal constraint
[and
    [= a.running false]
]

// global constraint
[and
    // - target: "pc.refer.running"
    // - base: the longest namespace where [base][0] = val
    // - the rest is split by "."
    //     rest = [r0, r1, r2, ..., rm, rn]
    // - basex = base
    // - values = {}
    // TODO: recursive function here
    // - for r in rest from r0 until rm, do
    //     base = base + "." + r
    //     type = [base][1]
    //     find-all x in initial state where
    //     (x[0] = val) and (type is member of x[1])
    //        vals = vals union ([= base x])
    //        values = values union vals
    // - 
    //
    // possible value of pc.refer: [a, b]
    // based on initial state: [pc][2][refer][2]
    [or
        [and [= pc.refer a] [= a.running true]]
        [and [= pc.refer b] [= b.running true]]
    ]
]

Another thought:

set1 = { pc.refer = a, pc.refer = b }

<Service>.running = { true }
set2 = { a.running, b.running } X { true }
    = { a.running = true, b.running = true }

set3 = set1 X set2
    = { pc.refer ... ???

We shouldn't use cartesian product. Just need recursive function.