Uploaded image for project: 'Kieler Semantics'
  1. Kieler Semantics
  2. KISEMA-1595

Valued signals are mis-interpreted

    XMLWordPrintable

    Details

    • Type: Bug
    • Status: Closed
    • Priority: Minor
    • Resolution: Fixed
    • Affects Version/s: 1.1
    • Fix Version/s: Next Release
    • Component/s: SCCharts
    • Labels:
      None

      Description

      Consider the attached MWE (valsig.sctx). Contrary to my possible bogus intuition, we can't make it to state B. I'm assuming here that `b` refers to the tick and `val(b)` to the most recent value of `b`, similar to `current b` in some lustre dialects.

      That this might not just a problem in the simulation IDE can be seen by exporting to Promela. I've verified that `s` is never true, implying that the challenge is infeasable, by adding

      ltl doh { []!s }
      

      to the .pml and running spin. The same problem manifests itself when trying to emit a valued signal as in MWE (valsig2.sctx) as being "not asc-schedulable".

        Attachments

        1. valsig.sctx
          0.4 kB
        2. valsig2.sctx
          0.1 kB

          Issue Links

            Activity

              People

              Assignee:
              als Alexander Schulz-Rosengarten
              Reporter:
              Kai Kai Engelhardt
              Votes:
              0 Vote for this issue
              Watchers:
              2 Start watching this issue

                Dates

                Created:
                Updated:
                Resolved: