Dev (#2)

Added tchecker support.

public/locales/de/translation.json

@@ -13,6 +13,10 @@
   "manipulation.table.clockPlural": "Uhren",
   "manipulation.table.editLabel": "{{type}} bearbeiten",
   "manipulation.table.deleteLabel": "{{type}} löschen",
+  "manipulation.table.integerSingular": "Integer",
+  "manipulation.table.integerPlural": "Integers",
+  "manipulation.table.syncSingular": "Sync",
+  "manipulation.table.syncPlural": "Syncs",
   "locDialog.errorNameEmpty": "Name darf nicht leer sein",
   "locDialog.errorNameExists": "Name wird bereits verwendet",
   "locDialog.editLoc": "Ort bearbeiten",
@@ -23,6 +27,10 @@
   "locDialog.button.cancel": "Abbrechen",
   "locDialog.button.edit": "Speichern",
   "locDialog.button.add": "Hinzufügen",
+  "locDialog.button.addLabel": "Label hinzufügen",
+  "locDialog.isCommitted": "Committed",
+  "locDialog.isUrgent": "Urgent",
+  "locDialog.hasLabels": "Labels",
   "switchDialog.title.editSwitch": "Switch bearbeiten",
   "switchDialog.title.addSwitch": "Switch hinzufügen",
   "switchDialog.input.action": "Aktion",
@@ -31,15 +39,51 @@
   "switchDialog.input.resetClock": "{{clockName}} zurücksetzen",
   "switchDialog.error.action": "Aktion darf nicht leer sein",
   "switchDialog.hasGuard": "Guard",
+  "switchDialog.hasStatement": "Statement",
+  "switchDialog.button.addStatement": "Statement hinzufügen",
   "switchDialog.button.cancel": "Abbrechen",
   "switchDialog.button.edit": "Speichern",
   "switchDialog.button.add": "Hinzufügen",
   "switchDialog.switchAlreadyExists": "Es existiert bereits ein äquivalenter Switch.",
+  "integerDialog.title.editInteger": "Integer bearbeiten",
+  "integerDialog.title.addInteger": "Integer hinzufügen",
+  "integerDialog.name": "Name",
+  "integerDialog.size": "Größe",
+  "integerDialog.min": "Min",
+  "integerDialog.max": "Max",
+  "integerDialog.init": "Init",
+  "integerDialog.error.nameEmpty": "Name darf nicht leer sein",
+  "integerDialog.error.nameExists": "Name wird bereits verwendet",
+  "integerDialog.error.minMessage": "Min muss kleiner als Max sein",
+  "integerDialog.error.maxMessage": "Max muss größer als Min sein",
+  "integerDialog.error.initMessage": "Init muss im Intervall liegen",
+  "integerDialog.error.sizeMessage": "Größe muss mind. 1 sein",
+  "integerDialog.button.cancel": "Abbrechen",
+  "integerDialog.button.edit": "Speichern",
+  "integerDialog.button.add": "Hinzufügen",
+  "syncDialog.addSync": "Synchronisation hinzufügen",
+  "syncDialog.editSync": "Synchronisation bearbeiten",
+  "syncDialog.error.lessThanTwo": "Weniger als 2 Syncs",
+  "syncDialog.button.addSync": "Sync hinzufügen",
+  "syncDialog.button.cancel": "Abbrechen",
+  "syncDialog.button.edit": "Speichern",
+  "syncDialog.button.add": "Hinzufügen",
+  "sync.delete": "Sync löschen",
+  "sync.input.process": "Prozess",
+  "sync.input.event": "Aktion",
+  "sync.input.isWeakSync": "schwache Sync",
   "clauses.input.clock": "Uhr",
   "clauses.input.comparison": "Vergleich",
   "clauses.input.value": "Wert",
   "clauses.delete": "Klausel löschen",
   "clauses.button.addClause": "Klausel hinzufügen",
+  "freeClauses.input": "Freie Klausel",
+  "freeClauses.delete": "Freie Klausel löschen",
+  "freeClauses.button.addFreeClause": "Freie Klausel hinzufügen",
+  "labels.delete": "Label löschen",
+  "labels.input": "Label",
+  "statements.delete": "Statement löschen",
+  "statements.input": "Statement",
   "deleteClockConfirmDialog.title": "Löschen von Uhr {{clockName}} bestätigen",
   "deleteClockConfirmDialog.contentText": "Uhr {{clockName}} wird noch in mindestens einem Clock Constraint genutzt. Bist du sicher, dass du Uhr {{clockName}} löschen möchtest?",
   "deleteClockConfirmDialog.contentTextWarning": "Alle Klauseln, die diese Uhr nutzen, werden entfernt!",
@@ -50,7 +94,24 @@
   "clockDialog.input.name": "Name",
   "clockDialog.errorNameEmpty": "Name darf nicht leer sein",
   "clockDialog.errorNameExists": "Name wird bereits verwendet",
+  "clockDialog.input.size": "Größe",
+  "clockDialog.errorSizeInvalid": "Größe muss mind. 1 sein",
   "clockDialog.button.cancel": "Abbrechen",
   "clockDialog.button.edit": "Speichern",
-  "clockDialog.button.add": "Hinzufügen"
+  "clockDialog.button.add": "Hinzufügen",
+  "uploadButton.button": "Datei Hochladen",
+  "downloadButton.button": "System herunterladen",
+  "processSelection.error.emptyName": "Name darf nicht leer sein",
+  "processSelection.error.duplicateName": "Name wird bereits verwendet",
+  "processSelection.input": "Prozess eingeben",
+  "processSelection.button.add": "Prozess hinzufügen",
+  "processSelection.select": "Prozess auswählen",
+  "processSelection.button.delete": "Prozess löschen",
+  "systemSelection.error.emptyName": "Name darf nicht leer sein",
+  "systemSelection.error.duplicateName": "Name wird bereits verwendet",
+  "systemSelection.input": "System eingeben",
+  "systemSelection.button.add": "System hinzufügen",
+  "systemSelection.select": "System auswählen",
+  "systemSelection.button.delete": "System löschen",
+  "layoutButton.text": "Justieren"
 }

public/locales/en/translation.json

@@ -13,6 +13,10 @@
   "manipulation.table.clockPlural": "Clocks",
   "manipulation.table.editLabel": "Edit {{type}}",
   "manipulation.table.deleteLabel": "Delete {{type}}",
+  "manipulation.table.integerSingular": "Integer",
+  "manipulation.table.integerPlural": "Integers",
+  "manipulation.table.syncSingular": "Sync",
+  "manipulation.table.syncPlural": "Syncs",
   "locDialog.errorNameEmpty": "Name cannot be empty",
   "locDialog.errorNameExists": "Name already exists",
   "locDialog.editLoc": "Edit Location",
@@ -23,6 +27,10 @@
   "locDialog.button.cancel": "Cancel",
   "locDialog.button.edit": "Save",
   "locDialog.button.add": "Add",
+  "locDialog.button.addLabel": "Add Label",
+  "locDialog.isCommitted": "Committed",
+  "locDialog.isUrgent": "Urgent",
+  "locDialog.hasLabels": "Labels",
   "switchDialog.title.editSwitch": "Edit Switch",
   "switchDialog.title.addSwitch": "Add Switch",
   "switchDialog.input.action": "Action",
@@ -31,15 +39,51 @@
   "switchDialog.input.resetClock": "Reset {{clockName}}",
   "switchDialog.error.action": "Action cannot be empty",
   "switchDialog.hasGuard": "Has Guard",
+  "switchDialog.hasStatement": "Has Statement",
+  "switchDialog.button.addStatement": "Add Statement",
   "switchDialog.button.cancel": "Cancel",
   "switchDialog.button.edit": "Save",
   "switchDialog.button.add": "Add",
   "switchDialog.switchAlreadyExists": "There already exists an equivalent switch.",
+  "integerDialog.title.editInteger": "Edit Integer",
+  "integerDialog.title.addInteger": "Add Integer",
+  "integerDialog.name": "Name",
+  "integerDialog.size": "Size",
+  "integerDialog.min": "Min",
+  "integerDialog.max": "Max",
+  "integerDialog.init": "Init",
+  "integerDialog.error.nameEmpty": "Name cannot be empty",
+  "integerDialog.error.nameExists": "Name already exists",
+  "integerDialog.error.minMessage": "Min has to be smaller than Max",
+  "integerDialog.error.maxMessage": "Max has to be bigger than Min",
+  "integerDialog.error.initMessage": "Init has to be within the intervall",
+  "integerDialog.error.sizeMessage": "Size must be at least 1",
+  "integerDialog.button.cancel": "Cancel",
+  "integerDialog.button.edit": "Save",
+  "integerDialog.button.add": "Add",
+  "syncDialog.addSync": "Add Synchronization",
+  "syncDialog.editSync": "Edit Synchronization",
+  "syncDialog.error.lessThanTwo": "Less than 2 Syncs",
+  "syncDialog.button.addSync": "Add Sync",
+  "syncDialog.button.cancel": "Cancel",
+  "syncDialog.button.edit": "Save",
+  "syncDialog.button.add": "Add",
+  "sync.delete": "Delete Sync",
+  "sync.input.process": "Process",
+  "sync.input.event": "Action",
+  "sync.input.isWeakSync": "weak Sync",
   "clauses.input.clock": "Clock",
   "clauses.input.comparison": "Comparison",
   "clauses.input.value": "Value",
   "clauses.delete": "Delete Clause",
   "clauses.button.addClause": "Add Clause",
+  "freeClauses.input": "Free Clause",
+  "freeClauses.delete": "Delete Free Clause",
+  "freeClauses.button.addFreeClause": "Add Free Clause",
+  "labels.delete": "Delete Label",
+  "labels.input": "Label",
+  "statements.delete": "Delete Statement",
+  "statements.input": "Statement",
   "deleteClockConfirmDialog.title": "Confirm Clock Deletion",
   "deleteClockConfirmDialog.contentText": "Clock {{clockName}} is still being used in at least one clock constraint. Are you sure you want to delete clock {{clockName}}?",
   "deleteClockConfirmDialog.contentTextWarning": "All clauses using this clock will be deleted!",
@@ -50,7 +94,24 @@
   "clockDialog.input.name": "Name",
   "clockDialog.errorNameEmpty": "Name cannot be empty",
   "clockDialog.errorNameExists": "Name already exists",
+  "clockDialog.input.size": "Size",
+  "clockDialog.errorSizeInvalid": "Size must be at least 1",
   "clockDialog.button.cancel": "Cancel",
   "clockDialog.button.edit": "Save",
-  "clockDialog.button.add": "Add"
+  "clockDialog.button.add": "Add",
+  "uploadButton.button": "Upload File",
+  "downloadButton.button": "Download System",
+  "processSelection.error.emptyName": "Name cannot be empty",
+  "processSelection.error.duplicateName": "Name already exists",
+  "processSelection.input": "Enter New Process",
+  "processSelection.button.add": "Add Process",
+  "processSelection.select": "Select Process",
+  "processSelection.button.delete": "Discard Process",
+  "systemSelection.error.emptyName": "Name cannot be empty",
+  "systemSelection.error.duplicateName": "Name already exists",
+  "systemSelection.input": "Enter New System",
+  "systemSelection.button.add": "Add System",
+  "systemSelection.select": "Select System",
+  "systemSelection.button.delete": "Discard System",
+  "layoutButton.text": "Adjust"
 }

src/App.tsx

@@ -5,19 +5,36 @@ import { Box, Grid } from '@mui/material';
 import { useLayoutEffect, useRef, useState } from 'react';
 import { useAnalysisViewModel } from './viewmodel/AnalysisViewModel';
 import { AutomatonManipulation } from './view/AutomatonManipulation';
-import UploadButton from './view/UploadButton.tsx';
+import ProcessSelection from './view/ProcessSelection.tsx';
+import AutomatonDrawer from './view/AutomationDrawer.tsx';
+import { useOpenedSystems } from './viewmodel/OpenedSystems.ts';
+import { useOpenedProcesses } from './viewmodel/OpenedProcesses.ts';
+import LayoutButton from './view/LayoutButton.tsx';
 
 function App() {
   const viewModel = useAnalysisViewModel();
+  const openedSystems = useOpenedSystems();
+  const openedProcesses = useOpenedProcesses();
   const { t } = useTranslation();
 
   // calculate size of content elements so that content always fits the window size
   const headerRef = useRef<HTMLHeadingElement>(null);
+  const toolRef = useRef<HTMLDivElement>(null);
   const [contentHeight, setContentHeight] = useState(window.innerHeight);
+  const [toolbarHeight, setToolbarHeight] = useState(0);
 
   useLayoutEffect(() => {
     const updateContentHeight = () => {
       const headerEl = headerRef.current;
+      const toolEl = toolRef.current;
+      if (toolEl) {
+        const style = window.getComputedStyle(toolEl);
+        const marginTop = parseInt(style.marginTop, 10);
+        const marginBottom = parseInt(style.marginBottom, 10);
+        const totalToolBarHeight = toolEl.offsetHeight + marginTop + marginBottom;
+        setToolbarHeight(totalToolBarHeight);
+      }
+
       if (headerEl) {
         const style = window.getComputedStyle(headerEl);
         const marginTop = parseInt(style.marginTop, 10);
@@ -38,8 +55,12 @@ function App() {
       <h1 style={{ paddingLeft: '16px' }} ref={headerRef}>
         ⏰ {t('app.title')}
       </h1>
-      <UploadButton></UploadButton>
-      <Box sx={{ display: 'flex', height: `${contentHeight - 1}px`, overflow: 'hidden' }}>
+      <Box ref={toolRef} sx={{ display: 'flex', alignItems: 'center' }}>
+        <AutomatonDrawer viewModel={viewModel} openedSystems={openedSystems} openedProcesses={openedProcesses} />
+        <ProcessSelection viewModel={viewModel} openedSystems={openedSystems} openedProcesses={openedProcesses} />
+        <LayoutButton viewModel={viewModel} />
+      </Box>
+      <Box sx={{ display: 'flex', height: `${contentHeight - toolbarHeight - 1}px`, overflow: 'hidden' }}>
         <Grid container sx={{ height: '100%' }}>
           <Grid
             item
@@ -49,7 +70,7 @@ function App() {
             lg={3}
             sx={{ borderRight: '1px solid #ccc', paddingLeft: '16px', overflowY: 'auto', height: '100%' }}
           >
-            <AutomatonManipulation viewModel={viewModel} />
+            <AutomatonManipulation viewModel={viewModel} openedSystems={openedSystems} />
           </Grid>
           <Grid item xs={12} sm={8} md={9} lg={9} sx={{ overflowY: 'hidden', height: '100%' }}>
             <AutomatonVisualization viewModel={viewModel} />

src/index.css

@@ -58,23 +58,6 @@ button:focus-visible {
   display: none;
 }
 
-.uploadButton {
-  display: inline-block;
-  color: #444;
-  border: 1px solid #ccc;
-  background: #ddd;
-  box-shadow: 0 0 5px -1px rgba(0, 0, 0, 0.2);
-  cursor: pointer;
-  vertical-align: middle;
-  max-width: 100px;
-  padding: 5px;
-  text-align: center;
-}
-.uploadButton:active {
-  color: red;
-  box-shadow: 0 0 5px -1px rgba(0, 0, 0, 0.6);
-}
-
 @media (prefers-color-scheme: light) {
   :root {
     color: #213547;

src/model/ta/clock.ts

@@ -1,3 +1,4 @@
 export interface Clock {
   name: string;
+  size: number;
 }

src/model/ta/clockComparator.ts

@@ -1,5 +1,6 @@
 export enum ClockComparator {
-  EQ = '=',
+  EQ = '==',
+  NEQ = '≠',
   LEQ = '≤',
   GEQ = '≥',
   LESSER = '<',
@@ -10,10 +11,20 @@ export function parseClockComparator(input: string): ClockComparator {
   switch (input) {
     case '=':
       return ClockComparator.EQ;
+    case '==':
+      return ClockComparator.EQ;
+    case '!=':
+      return ClockComparator.NEQ;
+    case '≠':
+      return ClockComparator.NEQ;
     case '≤':
       return ClockComparator.LEQ;
+    case '<=':
+      return ClockComparator.LEQ;
     case '≥':
       return ClockComparator.GEQ;
+    case '>=':
+      return ClockComparator.GEQ;
     case '<':
       return ClockComparator.LESSER;
     case '>':
@@ -22,3 +33,22 @@ export function parseClockComparator(input: string): ClockComparator {
       throw Error(`parseClockComparator: input ${input} is not a valid clock comparator`);
   }
 }
+
+export function deParseClockComparator(input: ClockComparator): string {
+  switch (input) {
+    case ClockComparator.NEQ:
+      return '!=';
+    case ClockComparator.EQ:
+      return '==';
+    case ClockComparator.LEQ:
+      return '<=';
+    case ClockComparator.GEQ:
+      return '>=';
+    case ClockComparator.GREATER:
+      return '>';
+    case ClockComparator.LESSER:
+      return '<';
+    default:
+      throw Error(`deParseClockComparator: input ${input} is not a valid clock comparator`);
+  }
+}

src/model/ta/clockConstraint.ts

@@ -1,5 +1,7 @@
 import { Clause } from './clause.ts';
+import {FreeClause} from "./freeClause.ts";
 
 export interface ClockConstraint {
   clauses: Clause[];
+  freeClauses: FreeClause[];
 }

src/model/ta/freeClause.ts

@@ -0,0 +1,3 @@
+export interface FreeClause {
+    term: string;
+}

src/model/ta/integer.ts

@@ -0,0 +1,7 @@
+export interface Integer{
+    name: string;
+    size: number;
+    min: number;
+    max: number;
+    init: number;
+}

src/model/ta/location.ts

@@ -6,4 +6,8 @@ export interface Location {
   invariant?: ClockConstraint;
   xCoordinate: number;
   yCoordinate: number;
+  setLayout?: boolean;
+  committed?: boolean;
+  urgent?: boolean;
+  labels?: string[];
 }

src/model/ta/switch.ts

@@ -1,11 +1,13 @@
 import { ClockConstraint } from './clockConstraint';
 import { Clock } from './clock';
 import { Location } from './location';
+import { SwitchStatement } from "./switchStatement.ts";
 
 export interface Switch {
   source: Location;
   guard?: ClockConstraint;
   actionLabel: string;
   reset: Clock[];
+  statement?: SwitchStatement;
   target: Location;
 }

src/model/ta/switchStatement.ts

@@ -0,0 +1,5 @@
+import {FreeClause} from "./freeClause.ts";
+
+export interface SwitchStatement {
+    statements: FreeClause[];
+}