Merge pull request #308 from lisa-analyzer/stability

Stability domain implementation

Author: lucaneg

lisa/lisa-analyses/imp-testcases/numeric/numeric.imp

@@ -7,7 +7,7 @@ class tutorial {
         	b = b + c;
    		return b;
     }
-    
+
 	sign_parity_example() {
 		def i = 2;
 		def max = 10;

lisa/lisa-analyses/imp-testcases/stability/report.json

@@ -0,0 +1,44 @@
+{
+  "warnings" : [ {
+    "message" : "['imp-testcases/stability/stability.imp':18:4] on 'untyped stability::scale(stability* this, untyped x, untyped y, untyped width, untyped height, untyped scale1, untyped scale2)': [STATEMENT] Classes computed: {  #TOP#: (height, width),  =: (scale1, scale2),  ↑=: (x, y)}"
+  }, {
+    "message" : "['imp-testcases/stability/stability.imp':2:1] on 'untyped stability::example(stability* this, untyped x, untyped y)': [STATEMENT] Classes computed: {  ↑=: (y),  ↓=: (x)}"
+  }, {
+    "message" : "['imp-testcases/stability/stability.imp':9:1] on 'untyped stability::send(stability* this, untyped dest, untyped amount, untyped sbalance, untyped dbalance)': [STATEMENT] Classes computed: {  =: (amount, dest),  ↑=: (dbalance),  ↓=: (sbalance)}"
+  } ],
+  "files" : [ "report.json", "untyped_stability.example(stability__this,_untyped_x,_untyped_y).json", "untyped_stability.scale(stability__this,_untyped_x,_untyped_y,_untyped_width,_untyped_height,_untyped_scale1,_untyped_scale2).json", "untyped_stability.send(stability__this,_untyped_dest,_untyped_amount,_untyped_sbalance,_untyped_dbalance).json" ],
+  "info" : {
+    "cfgs" : "3",
+    "duration" : "699ms",
+    "end" : "2024-07-30T11:04:55.372+02:00",
+    "expressions" : "94",
+    "files" : "3",
+    "globals" : "0",
+    "members" : "3",
+    "programs" : "1",
+    "start" : "2024-07-30T11:04:54.673+02:00",
+    "statements" : "21",
+    "units" : "1",
+    "version" : "0.1b8",
+    "warnings" : "3"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "WorstCasePolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "CoContraVarianceCheck",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "test-outputs/stability"
+  }
+}

lisa/lisa-analyses/imp-testcases/stability/stability.imp

@@ -0,0 +1,37 @@
+class stability {
+	example(x, y) {
+		while (x > 0 && y > 0) {
+			y = 2 * y;
+			x = x - 1;
+		}
+	}
+	
+	send(dest, amount, sbalance, dbalance) {
+		// hack: we force the typing to numeric to avoid having + being rewritten as strcat
+		dbalance  = dbalance - 0;
+		if (amount > 0 && amount <= sbalance) {
+			sbalance = sbalance - amount;
+			dbalance = dbalance + amount;
+		}
+	}
+
+    scale(x, y, width, height, scale1, scale2){
+		// hack: we force the typing to numeric to avoid having + being rewritten as strcat
+		x  = x - 0;
+		width  = width - 0;
+		
+    	if (x >= 0 && y >= 0 && width > 0 && height > 0 && scale1 > 0 && scale2 > 0){
+            def upperRightPointX = x + width;
+            def lowerLeftPointY = y - height;
+
+            x = x * scale1;
+            y = y * scale2;
+
+            upperRightPointX = upperRightPointX * scale1;
+            lowerLeftPointY = lowerLeftPointY * scale2;
+
+            width = x - upperRightPointX;
+            height = y - lowerLeftPointY;
+        }
+    }
+}

lisa/lisa-analyses/imp-testcases/stability/untyped_stability.example(stability__this,_untyped_x,_untyped_y).json

@@ -0,0 +1 @@
+{"name":"untyped stability::example(stability* this, untyped x, untyped y)","description":null,"nodes":[{"id":0,"subNodes":[1,4],"text":"&&(>(x, 0), >(y, 0))"},{"id":1,"subNodes":[2,3],"text":">(x, 0)"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":">(y, 0)"},{"id":5,"text":"y"},{"id":6,"text":"0"},{"id":7,"subNodes":[8,9],"text":"y = *(2, y)"},{"id":8,"text":"y"},{"id":9,"subNodes":[10,11],"text":"*(2, y)"},{"id":10,"text":"2"},{"id":11,"text":"y"},{"id":12,"subNodes":[13,14],"text":"x = -(x, 1)"},{"id":13,"text":"x"},{"id":14,"subNodes":[15,16],"text":"-(x, 1)"},{"id":15,"text":"x"},{"id":16,"text":"1"},{"id":17,"text":"ret"}],"edges":[{"sourceId":0,"destId":7,"kind":"TrueEdge"},{"sourceId":0,"destId":17,"kind":"FalseEdge"},{"sourceId":7,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":0,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x > 0 && y > 0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":1,"description":{"expressions":["x > 0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":4,"description":{"expressions":["y > 0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":6,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":7,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"↑"}}}}},{"nodeId":8,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":9,"description":{"expressions":["2 * y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":10,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":["float32","int32"],"y":["float32","int32"]},"value":{"aux":{"x":"[0, +Inf]","y":"[2, +Inf]"},"trends":{"x":"↓","y":"="}}}}},{"nodeId":13,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":14,"description":{"expressions":["x - 1"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":16,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":17,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}}]}

lisa/lisa-analyses/imp-testcases/stability/untyped_stability.scale(stability__this,_untyped_x,_untyped_y,_untyped_width,_untyped_height,_untyped_scale1,_untyped_scale2).json

@@ -0,0 +1 @@
+{"name":"untyped stability::send(stability* this, untyped dest, untyped amount, untyped sbalance, untyped dbalance)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"dbalance = -(dbalance, 0)"},{"id":1,"text":"dbalance"},{"id":2,"subNodes":[3,4],"text":"-(dbalance, 0)"},{"id":3,"text":"dbalance"},{"id":4,"text":"0"},{"id":5,"subNodes":[6,9],"text":"&&(>(amount, 0), <=(amount, sbalance))"},{"id":6,"subNodes":[7,8],"text":">(amount, 0)"},{"id":7,"text":"amount"},{"id":8,"text":"0"},{"id":9,"subNodes":[10,11],"text":"<=(amount, sbalance)"},{"id":10,"text":"amount"},{"id":11,"text":"sbalance"},{"id":12,"subNodes":[13,14],"text":"sbalance = -(sbalance, amount)"},{"id":13,"text":"sbalance"},{"id":14,"subNodes":[15,16],"text":"-(sbalance, amount)"},{"id":15,"text":"sbalance"},{"id":16,"text":"amount"},{"id":17,"subNodes":[18,19],"text":"dbalance = +(dbalance, amount)"},{"id":18,"text":"dbalance"},{"id":19,"subNodes":[20,21],"text":"+(dbalance, amount)"},{"id":20,"text":"dbalance"},{"id":21,"text":"amount"},{"id":22,"text":"ret"}],"edges":[{"sourceId":0,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":12,"kind":"TrueEdge"},{"sourceId":5,"destId":22,"kind":"FalseEdge"},{"sourceId":12,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":22,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":1,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":2,"description":{"expressions":["dbalance - 0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":3,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":4,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":5,"description":{"expressions":["amount > 0 && amount <= sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":6,"description":{"expressions":["amount > 0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":7,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":8,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":9,"description":{"expressions":["amount <= sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":10,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":11,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":12,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"↓"}}}}},{"nodeId":13,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":14,"description":{"expressions":["sbalance - amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":15,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":16,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":17,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"↑","dest":"=","sbalance":"="}}}}},{"nodeId":18,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":19,"description":{"expressions":["dbalance + amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":20,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":21,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":22,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}}]}