Abstract State Machines

Abstract state machines (ASMs) provide a high-level means for assembling complex transformation programs.

ASM functions

ASM functions provide a non-persistent map to store values. Each ASM function needs to be declared prior to its first use. Initial values can also be set when defining an ASM function. The values stored at a certain location of an ASM function can be updated using the update ASM construct (see later).

machine asmFuns {
 asmfunction team / 2 {
     // Initialization
 	(1, "real") = "Casillas";
 	(7, "real") = "Raul";
 	// Any values are allowed to be used in the untyped version
 	(7.1, 6) = 2;
 }

 asmfunction anotherFun / 1; // An ASM function without initialization
}

In the new (upcoming) VIATRA2 version, types can also be defined for ASM functions as follows.

 // Import is needed if types are intended to be used by local names
 import datatypes;
 machine asmFuns {
  asmfunction team(Integer, datatypes.String) : String  { // FQNs can always be used for defining types
 	(1, "real") = "Casillas";
 	(7, "real") = "Raul";
 	// The following initialization would be a type error
       // (7.1, 6) = 2;
  }

  rule main() = seq 
  {
 	update team(1, "mu") = "van der sar";
  }
 }

User defined ASM rules

Users can define ASM rules as means for encapsulating certain functionality as a reusable operation. A user-defined ASM rule has an arbitrary number of parameters with the following directions:

in: input parameter, which means (i) the parameter should be non-empty when calling the rule, and (ii) all updates of the corresponding parameter (variable) within the rule will be lost after the completion of the ASM rule.
out: output parameter, which means that (i) the value passed as input to an output parameter is ignored, but the effects of updates of an output variable are reflected after the completion of ASM rule
inout: input-output parameter, which means that an input value is passed to the ASM rule, and the effects of updates are reflected upon completion.

An optional type can be associated to each parameter of a user-defined ASM rule, which refers to an existing model element within the model space (i.e. existing at compile time).

 import datatypes;
 machine callrules_01{
  rule test(in X:String , out Y, inout Z) = seq { 
 	update Y = X+Z;
 	print(X + Y + Z); // prints "aacc"
  } 
  rule main() = seq{
 	call test("a", "b", "c"); 
  }
 }

The further use of user-defined ASM rules are illustrated in the following example:

 machine symParams
 {
  rule main() = seq
  {
	let A=1, B=2, C=undef in seq {
 		call myRule(A,B,C);
 		println(A + "," + B + "," +C); // 1,1,2
 		call myRule(3,B,C);
 		println(3 + "," + B + "," +C); // 3,3,6
 		call myRule(A,B,A); 
 		println(A + "," + B + "," +A); // 2,1,2
 	}
  }

  rule myRule(in A, inout B, out C) = seq
  {
 	update B = A;
 	update C = A + B;
  }
}

Simple rules

Simple rules include the following elementary ASM control structures:

skip: no operation
fail: execution is terminated along the given path (with a failure)
print(X), println(X): prints term X (simply, or as a separate line). Buffered output can be initiated by print(B, X) and println(B, X), where buffer variable B should be initialized by a previous call to getBuffer/1.
log(Sev, X): prints term X to the error log with severity Sev (error, info, warning, debug, fatal)
update X = Y, update fun(X) = Y: assigns a new value Y to variable X or ASM function location fun(X)
call asmRule(X): calls user-defined ASM rule with actual parameter X

 machine simple_rules {
  rule main(in X) = seq {
	skip; 
 	print("abc"); 
 	log(error, "Error");
 	update X = "sec";
  }
 }

Composite rules

Composite rules allow to assemble more complex transformation algorithms. Composite control structures in VTCL are as follows:

if © R1 else R2: If condition C holds then executes R1, else executes R2; fails if the selected execution branch fails; ( else part is optional)
try R1 else R2: Executes R1, and if its execution fails, then it executes R2 (where the else part is optional); try/else rule fails if R2 fails, try rule (without else) fails when R1 fails
seq {R1; R2;}: Executes R1 and R2 in this specific order. Sequential rule fails if either R1 or R2 fails.
random {R1; R2; }: Non-deterministically selects R1 or R2, and executes it. Random rule fails if the selected rule (R1 or R2) fails.
let X = t1, Y= t2 in R1: Defines new variables X and Y, and initializes them with values t1 and t2, respectively, then rule R1 is executed. The let rule fails if the execution of R1 fails.
choose X with C(X) do R: Computes an assignment of variable X, which fulfills condition C (where X appears in a pattern call, a GT rule application or in an ASM function). If a valid binding exists, then executes rule R, otherwise the choose rule fails. The choose rule also fails if the execution of rule R fails.
forall X with C(X) do R: Computes all assignments of variable X, which fulfills condition C (where X appears in a pattern call, a GT rule application or in an ASM function). Then it executes rule R for all valid assignments. The forall rule never fails (even if no valid assigns are found) .
iterate R: executes rule R as long as possible, i.e. it subsequently calls rule R until the final execution of R fails. Note that this rule can cause non-termination.

Example for using if rule

 machine ifrules_01{
  rule main (in X)= seq {
  	print(X);
 	if (X == 10) print("OK:if"); 
 	else print("ERR:else");
 	if (X != 10) print("ERR:if"); 
 	else print("OK:else");
  }
 }

Example for using try rule

 machine tryrules_01{
  rule testing(in X)= seq {
 	if (X == 4) fail;
 	print(X);
  }

  rule main ()= seq {
	try call testing(2); 
 	else print("ERR");

try call testing(4); else print("OK");

  }
 }

Example for choose rule with ASM functions as conditions (more examples will be given for GT patterns)

 import datatypes;
 machine chooserules_01{
 // Untyped version	
  asmfunction testFunc/1 {("a") = 1; ("b") = 2; ("c") = 3;}
  rule main() = seq{
 	choose Y with (testFunc(Y) > 1) do seq{
 		if (Y == "b" || Y == "c") print("OK");
 		else print("ERR");
 	}

call myRule1();

 // Typed version
  asmfunction testFunc2(String): Integer {("a") = 1; ("b") = 2; ("c") = 3;}
  rule myRule1() = seq{
 	choose Y: String with (testFunc(Y) > 1) do seq{
 		if (Y == "b" || Y == "c") print("OK");
 		else print("ERR");
 	}	
  }
 }

Example for forall rule with ASM functions as conditions (more examples will be given for GT patterns)

 machine forallrules_01{
  asmfunction testFunc/1 {("a") = 1; ("b") = 2; ("c") = 3;}
  rule main() = let C1 = false, C2 = false in seq{
 	forall Y with (testFunc(Y) > 1) do seq{
 		if (Y == "b") update C1 = true;			
 		if (Y == "c") update C2 = true;
 	}		
 	if (C1 == true && C2 == true) print("OK");
 	else print("ERR");
 	call forallRule1();	
  }

  asmfunction testFunc2 (datatypes.String) : datatypes.Integer {("a") = 1; ("b") = 2; ("c") = 3;}
  rule forallRule1 () = let C1 = false, C2 = false in seq{
 	forall Y with (testFunc2(Y) > 1) do seq{
 		if (Y == "b") update C1 = true;			
 		if (Y == "c") update C2 = true;
 	}		
 	if (C1 == true && C2 == true) print("OK");
 	else print("ERR");	
  }
 }