import datatypes; import serviceConfiguration.metamodel; @incremental machine serviceConfiguration{ pattern emptyNode(Node) = { empty(Node); } @goal('lowerbound' = '0') pattern upServiceNode(Node,Up) = { service(Node); service.up(Up,Node,Node); } @goal('lowerbound' = '3') pattern activeServiceNode(Node,Active) = { service(Node); service.active(Active,Node,Node); } pattern downServiceNode(Node,Down) = { service(Node); service.down(Down,Node,Node); } @goal('lowerbound' = '2') pattern standbyServiceNode(Node,Standby) = { service(Node); service.standby(Standby,Node,Node); } @globalconstraint('upperbound' = '7') pattern serviceWithType(Node,Type) = { service(Node); entity(NodeType); instanceOf(Node,NodeType); relation(TypeR,Node,Node); relation(Type,NodeType,NodeType); instanceOf(TypeR,Type); } @goal('lowerbound' = '2') pattern backupService(Primary,Backup) = { service(Primary); service(Backup); service.backup(BR,Primary,Backup); } /*@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); }*/ @goal // nomatching pattern anydown() = { service(S); service.down(R,S,S); } /*pattern moreThanNService() = { find serviceWithType(Service,Type) # N; check(N > 7); }*/ @labelingliteral('priority' = '1') 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('priority' = '2') 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('priority' = '3') 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); } } @labelingliteral('priority' = '3') 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('priority' = '4') gtrule removeServiceWBackup(in Service, out Node) = { precondition pattern downWithBackup(Service, S2, R, Rs, Down) = { //find downServiceNode(Service,Down); service(Service); service.down(Down,Service,Service); service(S2); service.standby(Rs,S2,S2); service.backup(R,Service,S2); } action { let Name = name(Service) in seq{ delete(R); delete(Down); //println("Service removed: " + Service); delete(Service); delete(Rs); //update servCounter() = toInteger(servCounter())-1; new(empty(Node) in model()); let Ru = undef in new(service.up(Ru,S2,S2)); //rename(Node,"e"+toString(emptyCounter())); rename(Node,Name); //update emptyCounter() = toInteger(emptyCounter())+1; } } } @labelingliteral('priority' = '7') 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('priority' = '8') 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.up(R,Service,Service)); //println("Service unregistered: " + Service); } } @labelingliteral('priority' = '9') 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)); } } } asmfunction model/0 {() = serviceConfiguration.models.test.conf;} //asmfunction servCounter/0 {() = 1;} //asmfunction emptyCounter/0 {() = 5;} pattern activeWNB(Service) = { service(Service); service.active(Active,Service,Service); neg pattern backup(Service) = { service(Service); service(S2); service.backup(R,Service,S2); } } //activeAmount = 2; //standbyAmount = 2; //upAmount = -1; //backupAmount = 2; //maxServAmount = 8; rule main(in MaxServA, in ServiceA, in ActiveA, in StandbyA, in DownA) = seq{ println("Service conf called"); //update model() = serviceConfiguration.models.test.conf; let Counter = 1, E = undef, R = undef in seq{ iterate seq{ if(Counter > MaxServA) fail; new(empty(E) in model()); update Counter = Counter+1; } update Counter = 1; iterate choose Node below model() with find emptyNode(Node) do seq{ if(Counter > ServiceA) fail; let Service = undef in try choose with apply powerOnService(Node, Service) do update Counter = Counter+1; } update Counter = 1; iterate choose S, Up below model() with find upServiceNode(S,Up) do seq{ if(Counter > (ActiveA + DownA)) fail; try choose with apply registerService(S) do update Counter = Counter+1; } update Counter = 1; iterate choose Service, Up below model() with find upServiceNode(Service,Up) do seq{ if(Counter > StandbyA) fail; try choose SA with find activeWNB(SA) do try choose with apply standbyService(SA,Service) do update Counter = Counter+1; } update Counter = 1; iterate choose S3, Standby below model() with find standbyServiceNode(S3,Standby) do seq{ if(Counter > DownA) fail; try choose SA,Active with find activeServiceNode(SA,Active) do seq{ delete(Active); new(service.down(R,SA,SA)); update Counter = Counter+1; } } } } }