Merge commit 'c6fb2930db09bc307a740034180b4d2a84bd92b1' into release

overturetool · Dec 4, 2013 · 6fb518a · 6fb518a
2 parents d910766 + c6fb293
commit 6fb518a
Show file tree

Hide file tree

Showing 20 changed files with 874 additions and 601 deletions.
diff --git a/documentation/examples/VDM++/HomeAutomationConc/BaseThread.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/BaseThread.vdmpp
@@ -0,0 +1,35 @@
+class BaseThread
+
+instance variables
+
+protected period : nat1 := 1;
+protected isPeriodic : bool := true;
+
+operations
+
+protected BaseThread : () ==> BaseThread
+BaseThread() ==
+ (World`timerRef.RegisterThread(self);
+  if(not World`timerRef.IsInitialising())
+  then start(self);  
+ );
+
+Step : () ==> ()
+Step() ==
+  is subclass responsibility
+
+thread
+ (if isPeriodic
+  then (while true
+        do 
+         (Step();
+          World`timerRef.WaitRelative(period);
+         )
+       )
+  else (Step();
+        World`timerRef.WaitRelative(0);
+        World`timerRef.UnRegisterThread();
+       )
+ );
+
+end BaseThread
diff --git a/documentation/examples/VDM++/HomeAutomationConc/Environment.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/Environment.vdmpp
@@ -2,6 +2,7 @@ class Environment is subclass of BaseThread
 
 instance variables
 
+--private ha       : HA;
 private io       : IO := new IO();
 private inlines	 : seq of inline := [];
 private simtime	 : nat := 1E9;
@@ -67,5 +68,20 @@ sync
 
   per IsFinished => finished;
 
+--thread
+-- (--World`timerRef.RegisterThread();
+--  --start(new ClockTick(threadid));
+--  while World`timerRef.GetTime() < simtime 
+--  do
+--   (--if(World`timerRef.GetTime() = 100)
+--    --then (testT := new TestThread(77, true);
+--    --     );
+--    if not finished
+--    then CreateSignal();
+
+--    World`timerRef.WaitRelative(1);
+--   );
+--  finished := true;
+-- )
 
 end Environment
diff --git a/documentation/examples/VDM++/HomeAutomationConc/HostController.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/HostController.vdmpp
@@ -214,4 +214,14 @@ sync
 per IsFinished => finished;
 per printStr => print;
 
+
+--thread
+-- (while true 
+--  do
+--   (UpdateValues();
+--    Algorithm();
+--    World`timerRef.WaitRelative(3);--World`timerRef.stepLength);
+--   )
+-- )
+
 end HostController
diff --git a/documentation/examples/VDM++/HomeAutomationConc/HumidSensor.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/HumidSensor.vdmpp
@@ -32,4 +32,14 @@ sync
 
   per IsFinished => finished;
 
+--thread
+-- (--World`timerRef.RegisterThread();
+
+--  while true 
+--  do 
+--   (Value := Env.ReadHumid();
+--    World`timerRef.WaitRelative(3);--World`timerRef.stepLength);
+--   )
+-- )
+
 end HumidSensor
diff --git a/documentation/examples/VDM++/HomeAutomationConc/TemperatureSensor.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/TemperatureSensor.vdmpp
@@ -32,4 +32,14 @@ sync
 
   per IsFinished => finished;
 
+--thread
+-- (--World`timerRef.RegisterThread();
+
+--  while true 
+--  do
+--   (Value := Env.ReadTemp();
+--    World`timerRef.WaitRelative(3);--World`timerRef.stepLength);
+--   )
+-- )
+
 end TemperatureSensor
diff --git a/documentation/examples/VDM++/HomeAutomationConc/Thermostat.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/Thermostat.vdmpp
@@ -45,4 +45,20 @@ sync
 
   per IsFinished => finished;
 
+--thread
+-- (--World`timerRef.RegisterThread();
+
+--  while true 
+--  do 
+--   (dcl tempCorr: NetworkTypes`correction := GetCorr();
+
+--    if tempCorr = <INC>
+--    then HA`Env.IncTemp()
+--    elseif tempCorr = <DEC>
+--    then HA`Env.DecTemp();
+
+--    World`timerRef.WaitRelative(5);--World`timerRef.stepLength);
+--   )
+-- )
+
 end Thermostat
diff --git a/documentation/examples/VDM++/HomeAutomationConc/Window.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/Window.vdmpp
@@ -41,4 +41,17 @@ sync
 
   per IsFinished => finished;
 
+--thread
+-- (--World`timerRef.RegisterThread();
+
+--  while true 
+--  do
+--   (if (GetCorr() = <OPEN>)
+--    then (HA`Env.DecHumid();
+--          HA`Env.DecTemp();
+--         );
+--    World`timerRef.WaitRelative(5);--World`timerRef.stepLength);
+--   )
+-- )
+
 end Window
diff --git a/documentation/examples/VDM++/HomeAutomationConc/World.vdmpp b/documentation/examples/VDM++/HomeAutomationConc/World.vdmpp
@@ -3,7 +3,7 @@ class World
 instance variables
 
 private env				: Environment;
-public static timerRef	: TimeStamp := new TimeStamp(); 
+public static timerRef	: TimeStamp := new TimeStamp(); --(6);
 private ha : HA;
 
 operations

diff --git a/documentation/examples/VDM++/MSAWconcur/BaseThread.vdmpp b/documentation/examples/VDM++/MSAWconcur/BaseThread.vdmpp
@@ -0,0 +1,35 @@
+class BaseThread
+
+instance variables
+
+protected period : nat1 := 1;
+protected isPeriodic : bool := true;
+
+operations
+
+protected BaseThread : () ==> BaseThread
+BaseThread() ==
+ (World`timerRef.RegisterThread(self);
+  if(not World`timerRef.IsInitialising())
+  then start(self);  
+ );
+
+Step : () ==> ()
+Step() ==
+  is subclass responsibility
+
+thread
+ (if isPeriodic
+  then (while true
+        do 
+         (Step();
+          World`timerRef.WaitRelative(period);
+         )
+       )
+  else (Step();
+        World`timerRef.WaitRelative(0);
+        World`timerRef.UnRegisterThread();
+       )
+ );
+
+end BaseThread
diff --git a/documentation/examples/VDM++/MSAWconcur/Radar.vdmpp b/documentation/examples/VDM++/MSAWconcur/Radar.vdmpp
@@ -102,6 +102,17 @@ measure set2seqFOm;
 set2seqFOm : set of FO -> nat
 set2seqFOm(fos) == card fos;
 
+--thread
+
+--while true do
+-- (
+--  let as = MSAW`airspace
+--  in
+--  (detected := { x.getId() |-> x | x in set as.getAirspace() & InRange(x) };
+--   UpdatePriorityList();
+--   World`timerRef.WaitRelative(TimeStamp`stepLength);
+--  )
+-- )
 
 sync 
 mutex(Step);