Merge branch 'master' of gitlab.henriktjader.com:pln/plcopen

examples/eq.rs

@@ -136,7 +136,11 @@ fn main() {
   }
 }
 
-fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
+fn periodic(
+  STATE: &mut State,
+  TIMEOUT_CNTR: &mut u32,
+  data: &Data,
+) {
   *STATE = match STATE {
     S8000 => match (data.a, data.b) {
       (F, F) => S8001,
@@ -163,8 +167,12 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
       _ => {
         *TIMEOUT_CNTR -= 1;
         match (data.a, data.b) {
-          (F, _) => S8001,
-          (_, T) => S8000,
+          (F, F) => S8001,
+          (F, T) => {
+            *TIMEOUT_CNTR = DISCREPANCY;
+            S8014
+          }
+          (T, T) => S8000,
           _ => S8004,
         }
       }
@@ -174,8 +182,12 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
       _ => {
         *TIMEOUT_CNTR -= 1;
         match (data.a, data.b) {
-          (_, F) => S8001,
-          (T, _) => S8000,
+          (F, F) => S8001,
+          (T, F) => {
+            *TIMEOUT_CNTR = DISCREPANCY;
+            S8004
+          }
+          (T, T) => S8000,
           _ => S8014,
         }
       }

examples/model.rs

@@ -21,7 +21,10 @@ impl<'a> Device<'a> {
     klee::kassume(v < 32);
     v
   }
-    pub unsafe fn write(&self, v: u32) {
+  pub unsafe fn write(
+    &self,
+    v: u32,
+  ) {
     klee::kassert!(v < 32);
     let v = self.ptr.write(v);
   }

examples/model2.rs

@@ -19,7 +19,10 @@ impl RegA {
     klee::kassume(v < 32);
     v
   }
-    pub unsafe fn write(&self, v: u32) {
+  pub unsafe fn write(
+    &self,
+    v: u32,
+  ) {
     klee::kassert!(v < 32);
     let v = self.0.write(v);
   }
@@ -37,7 +40,10 @@ impl RegB {
       STATE
     }
   }
-    pub unsafe fn write(&self, v: u32) {
+  pub unsafe fn write(
+    &self,
+    v: u32,
+  ) {
     STATE = v;
   }
 }

examples/model3.rs

@@ -28,7 +28,10 @@ impl RegC {
     }
     v
   }
-    pub unsafe fn write(&self, v: u32) {
+  pub unsafe fn write(
+    &self,
+    v: u32,
+  ) {
     OLD_STATE = v;
   }
 }

examples/model4.rs

@@ -27,7 +27,10 @@ impl RegC {
     }
   }
 
-    pub unsafe fn write(&self, v: u32) {
+  pub unsafe fn write(
+    &self,
+    v: u32,
+  ) {
     OLD_STATE = v;
   }
 }

rustfmt.toml

+tab_spaces = 2
+fn_args_density = "Vertical"

src/main.rs

@@ -85,7 +85,11 @@ const DISCREPENCY: u32 = 4;
 const T: bool = true;
 const F: bool = false;
 
-fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
+fn periodic(
+  STATE: &mut State,
+  TIMEOUT_CNTR: &mut u32,
+  DATA: &mut Data,
+) {
   // we start directly in the init state S80001
   // static mut STATE: State = State::S8001;
   // static mut TIMEOUT_CNTR: u32 = 0;