bug fix

diff --git a/Robust/src/Benchmarks/Performance/Dispatch.java b/Robust/src/Benchmarks/Performance/Dispatch.java
index b3fe20fc1f28f367777d1df24c81d2c93aa688e2..80206913d0fac5c0e9a53b227e8f88abf90ddbc3 100644 (file)
--- a/Robust/src/Benchmarks/Performance/Dispatch.java
+++ b/Robust/src/Benchmarks/Performance/Dispatch.java
@@ -1,10 +1,10 @@
 task start(StartupObject s {initialstate}) {
-    Foo f=new Foo(){run};
-    
+    Dispatch f=new Dispatch(){run};
+   
     taskexit(s{!initialstate});
 }
 
-task DoOperation(Foo f{run}) {
+task DoOperation(Dispatch f{run}) {
     if (f.count==1000000)
        taskexit(f{!run});
     else {
@@ -13,9 +13,9 @@ task DoOperation(Foo f{run}) {
     }
 }
 
-public class Foo {
+public class Dispatch {
     flag run;
     int count;
-    public Foo() {
+    public Dispatch() {
     }
 }
\ No newline at end of file