import datatypes; import serviceConfiguration.metamodel; machine serviceConfiguration{ pattern emptyNode(Node) = { empty(Node); } pattern upServiceNode(Node,Up) = { service(Node); service.up(Up,Node,Node); } pattern activeServiceNode(Node,Active) = { service(Node); service.active(Active,Node,Node); } pattern downServiceNode(Node,Down) = { service(Node); service.down(Down,Node,Node); } pattern standbyServiceNode(Node,Standby) = { service(Node); service.standby(Standby,Node,Node); } /*@goal('fixnumber' = '1') pattern properServiceConfiguration() = { service(S1); service.up(U1,S1,S1); service(S2); service.up(U2,S2,S2); service(S3); service.active(A3,S3,S3); service(S4); service.active(A4,S4,S4); }*/ @goal('fixnumber' = '1') pattern properServiceConfiguration() = { service(S1); service.standby(U1,S1,S1); service(S2); service.standby(U2,S2,S2); service(S3); service.active(A3,S3,S3); service.backup(B3,S3,S1); service(S4); service.active(A4,S4,S4); service.backup(B4,S4,S2); service(S5); service.active(A5,S5,S5); neg pattern anydown() = { service(S); service.down(R,S,S); } } @labelingliteral gtrule powerOnService(in Node, out Service) = { precondition find emptyNode(Node) action { let Name = name(Node) in seq{ delete(Node); //update emptyCounter() = toInteger(emptyCounter())-1; new(service(Service) in model()); //rename(Service,"s"+toString(servCounter())); rename(Service,Name); //update servCounter() = toInteger(servCounter())+1; //println("Service created: " + Service); let R = undef in new(service.up(R,Service,Service)); } } } @labelingliteral gtrule removeService(in Service, out Node) = { precondition pattern downWithNoBackup(Service, Down) = { //find downServiceNode(Service,Down); service(Service); service.down(Down,Service,Service); neg pattern backup(Service) = { service(Service); service(S2); service.standby(Rs,S2,S2); service.backup(R,Service,S2); } } action { let Name = name(Service) in seq{ delete(Down); //println("Service removed: " + Service); delete(Service); //update servCounter() = toInteger(servCounter())-1; new(empty(Node) in model()); //rename(Node,"e"+toString(emptyCounter())); rename(Node,Name); //update emptyCounter() = toInteger(emptyCounter())+1; } } } @labelingliteral gtrule registerService(inout Service) = { precondition find upServiceNode(Service,Up) action { delete(Up); let R = undef in new(service.active(R,Service,Service)); //println("Service registered: " + Service); } } @labelingliteral gtrule unregisterService(inout Service) = { precondition pattern activeWithNoBackup(Service, Active) = { //find activeServiceNode(Service,Active); service(Service); service.active(Active,Service,Service); neg pattern backup(Service) = { service(Service); service(S2); service.backup(R,Service,S2); } } action { delete(Active); let R = undef in new(service.active(R,Service,Service)); //println("Service unregistered: " + Service); } } @labelingliteral gtrule standbyService(inout Service, inout Service2) = { precondition pattern standbyNodes(Service, Service2, Up) = { //find activeServiceNode(Service,Active); //find upServiceNode(Service2,Up); service(Service); service.active(Active,Service,Service); service(Service2); service.up(Up,Service2,Service2); } action { delete(Up); let R = undef in new(service.standby(R,Service2,Service2)); let R = undef in new(service.backup(R,Service,Service2)); //println("Service to standby: " + Service2 + ", backup for: " + Service); } } @labelingliteral gtrule detachService(inout Service, inout Service2) = { precondition pattern standbyNodes(Service, Service2, Standby, Backup) = { //find activeServiceNode(Service,Active); //find standbyServiceNode(Service2,Standby); service(Service); service.active(Active,Service,Service); service(Service2); service.standby(Standby,Service2,Service2); service.backup(Backup,Service,Service2); } action { delete(Standby); delete(Backup); let R = undef in new(service.up(R,Service2,Service2)); //println("Service detached: " + Service2 + ", was backup for: " + Service); } } @labelingliteral gtrule failoverService(inout Service, inout Service2) = { precondition pattern standbyNodes(Service, Service2, Standby, Backup) = { //find downServiceNode(Service,Down); //find standbyServiceNode(Service2,Standby); service(Service); service.down(Down,Service,Service); service(Service2); service.standby(Standby,Service2,Service2); service.backup(Backup,Service,Service2); } action { delete(Standby); delete(Backup); let R = undef in new(service.active(R,Service2,Service2)); //println("Service failover: " + Service2 + ", was backup for: " + Service); } } asmfunction model/0 {() = serviceConfiguration.models.test.conf;} //asmfunction servCounter/0 {() = 1;} //asmfunction emptyCounter/0 {() = 5;} rule main() = seq{ println("Service conf called"); //update model() = serviceConfiguration.models.test.conf; let SwB = undef, SwB2 = undef in seq{ iterate choose Node below model() with find emptyNode(Node) do let Service = undef in try choose with apply powerOnService(Node, Service) do skip; /*try choose S, Up below model() with find upServiceNode(S,Up) do try choose with apply registerService(S) do seq{ update SwB = S; } try choose S, Up below model() with find upServiceNode(S,Up) do try choose with apply registerService(S) do seq{ update SwB2 = S; } try choose Service, Up below model() with find upServiceNode(Service,Up) do try choose with apply standbyService(SwB,Service) do skip; try choose Service, Up below model() with find upServiceNode(Service,Up) do try choose with apply standbyService(SwB2,Service) do skip; try choose S3, Standby below model() with find standbyServiceNode(S3,Standby) do try choose with apply detachService(SwB2, S3) do skip; */ forall S,U below model() with find upServiceNode(S,U) do let R = undef in seq{ delete(U); new(service.down(R,S,S)); println("Service went down: " + S); } /* iterate choose S3, Standby below model() with find standbyServiceNode(S3,Standby) do try choose with apply failoverService(SwB, S3) do skip; */ iterate choose SD, Down below model() with find downServiceNode(SD,Down) do let ND = undef in try choose with apply removeService(SD, ND) do skip; } } }