Skip to content

Commit

Permalink
added reachability check to UI
Browse files Browse the repository at this point in the history
  • Loading branch information
@luth1um
luth1um committed Aug 29, 2024
1 parent 106a58c commit fe6dfb1
Show file tree
Hide file tree
Showing 7 changed files with 187 additions and 10 deletions.
2 changes: 1 addition & 1 deletion e2e/helper/utilHelper.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ export class UtilHelper {

async findAllElementsWithPartialTestId(partialTestId: string): Promise<ElementHandle<SVGElement | HTMLElement>[]> {
// briefly pause to ensure that all elements are loaded
await this.page.waitForTimeout(100);
await this.page.waitForTimeout(200);
return await this.page.$$(`[data-testid^="${partialTestId}"]`);
}
}
8 changes: 8 additions & 0 deletions public/locales/de/translation.json
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{
"app.title": "Analyse von Timed Automata",
"manipulation.button.reachability": "Erreichbarkeit",
"manipulation.table.showContent": "{{content}} ausklappen",
"manipulation.table.hideContent": "{{content}} einklappen",
"manipulation.table.addElement": "{{content}} hinzufügen",
Expand All @@ -13,6 +14,13 @@
"manipulation.table.clockPlural": "Uhren",
"manipulation.table.editLabel": "{{type}} bearbeiten",
"manipulation.table.deleteLabel": "{{type}} löschen",
"analysisDialog.title": "Erreichbarkeitsanalyse",
"analysisDialog.description": "An dieser Stelle kann eine Erreichbarkeitsanalyse für den modellieren TA durchgeführt werden. Als Ergebnis werden alle unerreichbaren Orte aufgelistet.",
"analysisDialog.analysis.error": "Bei der Analyse ist ein Fehler aufgetreten. {{msg}}",
"analysisDialog.analysis.resultAllReachable": "Alle Orte sind erreichbar.",
"analysisDialog.analysis.resultSomeUnreachable": "Die folgenden Orte sind unerreichbar:",
"analysisDialog.button.close": "Schließen",
"analysisDialog.button.analyze": "Starten",
"locDialog.errorNameEmpty": "Name darf nicht leer sein",
"locDialog.errorNameExists": "Name wird bereits verwendet",
"locDialog.editLoc": "Ort bearbeiten",
Expand Down
8 changes: 8 additions & 0 deletions public/locales/en/translation.json
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{
"app.title": "Timed-Automata Analysis",
"manipulation.button.reachability": "Reachability",
"manipulation.table.showContent": "Show {{content}}",
"manipulation.table.hideContent": "Hide {{content}}",
"manipulation.table.addElement": "Add {{content}}",
Expand All @@ -13,6 +14,13 @@
"manipulation.table.clockPlural": "Clocks",
"manipulation.table.editLabel": "Edit {{type}}",
"manipulation.table.deleteLabel": "Delete {{type}}",
"analysisDialog.title": "Analyze Reachability",
"analysisDialog.description": "Here, you start a reachability analysis for the TA. As a result, all unreachable locations will be listed.",
"analysisDialog.analysis.error": "An error occurred during analysis. {{msg}}",
"analysisDialog.analysis.resultAllReachable": "All locations are reachable.",
"analysisDialog.analysis.resultSomeUnreachable": "The following locations are unreachable:",
"analysisDialog.button.close": "Close",
"analysisDialog.button.analyze": "Analyze",
"locDialog.errorNameEmpty": "Name cannot be empty",
"locDialog.errorNameExists": "Name already exists",
"locDialog.editLoc": "Edit Location",
Expand Down
104 changes: 104 additions & 0 deletions src/view/AnalysisDialog.tsx
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
import { Button, Dialog, DialogActions, DialogContent, DialogTitle, IconButton } from '@mui/material';
import CloseIcon from '@mui/icons-material/Close';
import { useButtonUtils } from '../utils/buttonUtils';
import { findUnreachableLocations } from 'timed-automata-analyzer';
import { useAnalyzerMappingUtils } from '../utils/analyzerMappingUtils';
import { useState } from 'react';
import { useTranslation } from 'react-i18next';
import { AnalysisState, AnalysisViewModel } from '../viewmodel/AnalysisViewModel';

interface AnalysisDialogProps {
open: boolean;
viewModel: AnalysisViewModel;
handleClose: () => void;
}

export const AnalysisDialog: React.FC<AnalysisDialogProps> = (props) => {
const { open, viewModel, handleClose } = props;
const { state, ta, setStateAnalyzing, setStateReady } = viewModel;
const { t } = useTranslation();
const { executeOnKeyboardClick } = useButtonUtils();
const { mapTaToAnalyzerModel } = useAnalyzerMappingUtils();
const [analysisResult, setAnalysisResult] = useState<JSX.Element | undefined>(undefined);

const handleFormClose = () => {
if (state !== AnalysisState.READY) {
return;
}
handleClose();
setAnalysisResult(undefined);
};

const handleAnalysis = () => {
setStateAnalyzing(viewModel);
let unreachableLocs: string[] = [];
const mappedTa = mapTaToAnalyzerModel(ta);
try {
unreachableLocs = findUnreachableLocations(mappedTa);
setStateReady(viewModel);
} catch (error) {
setStateReady(viewModel);
setAnalysisResult(<p>{t('analysisDialog.analysis.error', { msg: error })}</p>);
return;
}

if (unreachableLocs.length === 0) {
setAnalysisResult(<p>{t('analysisDialog.analysis.resultAllReachable')}</p>);
} else {
const resultItems = unreachableLocs.map((loc, index) => <li key={'reach-result-' + index}>{loc}</li>);
const unreachableText = t('analysisDialog.analysis.resultSomeUnreachable');
setAnalysisResult(
<>
<p>{unreachableText}</p>
<ul>{resultItems}</ul>
</>
);
}
};

return (
<Dialog
open={open}
onClose={handleFormClose}
PaperProps={{
style: { minWidth: '450px' },
}}
>
<DialogTitle>
{t('analysisDialog.title')}
<IconButton
onMouseDown={handleFormClose}
onKeyDown={(e) => executeOnKeyboardClick(e.key, handleFormClose)}
sx={{ position: 'absolute', right: 8, top: 8, color: (theme) => theme.palette.grey[500] }}
disabled={state !== AnalysisState.READY}
>
<CloseIcon />
</IconButton>
</DialogTitle>
<DialogContent>
<p>{t('analysisDialog.description')}</p>
{analysisResult}
</DialogContent>
<DialogActions>
<Button
onMouseDown={handleFormClose}
onKeyDown={(e) => executeOnKeyboardClick(e.key, handleFormClose)}
variant="contained"
color="error"
disabled={state !== AnalysisState.READY}
>
{t('analysisDialog.button.close')}
</Button>
<Button
onMouseDown={handleAnalysis}
onKeyDown={(e) => executeOnKeyboardClick(e.key, handleAnalysis)}
variant="contained"
color="primary"
disabled={state !== AnalysisState.READY}
>
{t('analysisDialog.button.analyze')}
</Button>
</DialogActions>
</Dialog>
);
};
40 changes: 34 additions & 6 deletions src/view/AutomatonManipulation.tsx
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import React, { useCallback, useMemo, useState } from 'react';
import { AnalysisViewModel } from '../viewmodel/AnalysisViewModel';
import { Tooltip, Typography } from '@mui/material';
import { AnalysisState, AnalysisViewModel } from '../viewmodel/AnalysisViewModel';
import { Button, Tooltip, Typography } from '@mui/material';
import ElementTable, { ElementRowData } from './ElementTable';
import { useTranslation } from 'react-i18next';
import { useFormattingUtils } from '../utils/formattingUtils';
Expand All @@ -14,6 +14,8 @@ import { Clock } from '../model/ta/clock';
import { useClockConstraintUtils } from '../utils/clockConstraintUtils';
import ClockDeleteConfirmDialog from './ClockDeleteConfirmDialog';
import ManipulateClockDialog from './ManipulateClockDialog';
import { AnalysisDialog } from './AnalysisDialog';
import { useButtonUtils } from '../utils/buttonUtils';

interface ManipulationProps {
viewModel: AnalysisViewModel;
Expand All @@ -22,6 +24,7 @@ interface ManipulationProps {
export const AutomatonManipulation: React.FC<ManipulationProps> = (props) => {
const { viewModel } = props;
const {
state,
ta,
addLocation,
editLocation,
Expand All @@ -37,6 +40,7 @@ export const AutomatonManipulation: React.FC<ManipulationProps> = (props) => {
const { t } = useTranslation();
const { formatLocationLabelTable, formatSwitchTable } = useFormattingUtils();
const { taUsesClockInAnyConstraint } = useClockConstraintUtils();
const { executeOnKeyboardClick } = useButtonUtils();

const [locationAddOpen, setLocationAddOpen] = useState(false);
const [locationEditOpen, setLocationEditOpen] = useState(false);
Expand Down Expand Up @@ -115,12 +119,13 @@ export const AutomatonManipulation: React.FC<ManipulationProps> = (props) => {
contentSingular={t('manipulation.table.locSingular')}
contentPlural={t('manipulation.table.locPlural')}
typeForTestId={'location'}
state={state}
onAddOpen={handleLocationAddOpen}
onEditOpen={handleLocationEditOpen}
onDelete={handleLocationDelete}
/>
);
}, [locations, t, formatLocationLabelTable, handleLocationEditOpen, handleLocationDelete]);
}, [locations, t, state, formatLocationLabelTable, handleLocationEditOpen, handleLocationDelete]);

// ===== manipulate switches =================================================

Expand Down Expand Up @@ -179,12 +184,13 @@ export const AutomatonManipulation: React.FC<ManipulationProps> = (props) => {
contentSingular={t('manipulation.table.switchSingular')}
contentPlural={t('manipulation.table.switchPlural')}
typeForTestId={'switch'}
state={state}
onAddOpen={handleSwitchAddOpen}
onEditOpen={handleSwitchEditOpen}
onDelete={handleSwitchDelete}
/>
);
}, [switches, t, formatSwitchTable, handleSwitchEditOpen, handleSwitchDelete]);
}, [switches, t, state, formatSwitchTable, handleSwitchEditOpen, handleSwitchDelete]);

// ===== manipulate clocks ===================================================

Expand Down Expand Up @@ -244,14 +250,15 @@ export const AutomatonManipulation: React.FC<ManipulationProps> = (props) => {
contentSingular={t('manipulation.table.clockSingular')}
contentPlural={t('manipulation.table.clockPlural')}
typeForTestId={'clock'}
state={state}
onAddOpen={handleClockAddOpen}
onEditOpen={handleClockEditOpen}
onDelete={handleClockDelete}
/>
);
}, [clocks, t, handleClockEditOpen, handleClockDelete]);
}, [clocks, t, state, handleClockEditOpen, handleClockDelete]);

// ===========================================================================
// ===== generate tables =====================================================

const allTables: JSX.Element[] = useMemo(() => {
const tables = [locationTable, switchTable, clockTable];
Expand All @@ -262,9 +269,30 @@ export const AutomatonManipulation: React.FC<ManipulationProps> = (props) => {
));
}, [locationTable, switchTable, clockTable]);

// ===== handle analysis =====================================================

const [analysisOpen, setAnalysisOpen] = useState(false);
const handleAnalysisOpen = () => setAnalysisOpen(true);
const handleAnalysisClose = () => setAnalysisOpen(false);

// ===========================================================================

return (
<>
<div key={'analysis-button-div'} style={{ marginBottom: '16px' }}>
<Button
onMouseDown={handleAnalysisOpen}
onKeyDown={(e) => executeOnKeyboardClick(e.key, handleAnalysisClose)}
variant="contained"
color="primary"
size="small"
disabled={state !== AnalysisState.READY}
>
{t('manipulation.button.reachability')}
</Button>
</div>
{allTables}
<AnalysisDialog open={analysisOpen} viewModel={viewModel} handleClose={handleAnalysisClose} />
<ManipulateLocationDialog
open={locationAddOpen}
locations={locations}
Expand Down
20 changes: 18 additions & 2 deletions src/view/ElementTable.tsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import { useTranslation } from 'react-i18next';
import { Add } from '@mui/icons-material';
import { Tooltip } from '@mui/material';
import { useButtonUtils } from '../utils/buttonUtils';
import { AnalysisState } from '../viewmodel/AnalysisViewModel';

export interface ElementRowData {
id: number;
Expand All @@ -27,13 +28,14 @@ interface ElementTableProps {
contentSingular: string;
contentPlural: string;
typeForTestId: string;
state: AnalysisState;
onAddOpen: () => void;
onEditOpen: (id: number) => void;
onDelete: (id: number) => void;
}

export const ElementTable: React.FC<ElementTableProps> = (props) => {
const { rows, contentSingular, contentPlural, typeForTestId, onAddOpen, onEditOpen, onDelete } = props;
const { rows, contentSingular, contentPlural, typeForTestId, state, onAddOpen, onEditOpen, onDelete } = props;
const { t } = useTranslation();
const { executeOnKeyboardClick } = useButtonUtils();

Expand All @@ -60,6 +62,7 @@ export const ElementTable: React.FC<ElementTableProps> = (props) => {
onKeyDown={(e) => executeOnKeyboardClick(e.key, () => onEditOpen(row.id))}
size="small"
data-testid={`button-edit-${typeForTestId}-${row.id}`}
disabled={state !== AnalysisState.READY}
>
<Tooltip title={t('manipulation.table.editLabel', { type: contentSingular })}>
<EditIcon />
Expand All @@ -70,6 +73,7 @@ export const ElementTable: React.FC<ElementTableProps> = (props) => {
onKeyDown={(e) => executeOnKeyboardClick(e.key, () => onDelete(row.id))}
size="small"
data-testid={`button-delete-${typeForTestId}-${row.id}`}
disabled={state !== AnalysisState.READY}
>
<Tooltip title={t('manipulation.table.deleteLabel', { type: contentSingular })}>
<DeleteIcon />
Expand All @@ -79,7 +83,17 @@ export const ElementTable: React.FC<ElementTableProps> = (props) => {
<TableCell data-testid={`table-cell-${typeForTestId}-${row.id}`}>{row.displayName}</TableCell>
</TableRow>
));
}, [rows, styleActionsColumn, contentSingular, typeForTestId, t, onEditOpen, onDelete, executeOnKeyboardClick]);
}, [
rows,
styleActionsColumn,
contentSingular,
typeForTestId,
t,
state,
onEditOpen,
onDelete,
executeOnKeyboardClick,
]);

return (
<>
Expand All @@ -88,6 +102,7 @@ export const ElementTable: React.FC<ElementTableProps> = (props) => {
variant="text"
onMouseDown={toggleCollapse}
onKeyDown={(e) => executeOnKeyboardClick(e.key, toggleCollapse)}
disabled={state !== AnalysisState.READY}
data-testid={'button-hide-' + typeForTestId}
>
{collapseLabel}
Expand All @@ -101,6 +116,7 @@ export const ElementTable: React.FC<ElementTableProps> = (props) => {
size="small"
onMouseDown={onAddOpen}
onKeyDown={(e) => executeOnKeyboardClick(e.key, onAddOpen)}
disabled={state !== AnalysisState.READY}
data-testid={'button-add-' + typeForTestId}
>
{t('manipulation.table.addElement', { content: contentSingular })}
Expand Down
15 changes: 14 additions & 1 deletion src/viewmodel/AnalysisViewModel.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ export interface AnalysisViewModel {
addClock: (viewModel: AnalysisViewModel, clockName: string) => void;
editClock: (viewModel: AnalysisViewModel, clockName: string, prevClockName: string) => void;
removeClock: (viewModel: AnalysisViewModel, clock: Clock) => void;
setStateAnalyzing: (viewModel: AnalysisViewModel) => void;
setStateReady: (viewModel: AnalysisViewModel) => void;
}

export enum AnalysisState {
Expand Down Expand Up @@ -277,6 +279,16 @@ export function useAnalysisViewModel(): AnalysisViewModel {
[removeAllClausesUsingClock, removeClockFromAllResets]
);

const setStateAnalyzing = useCallback((viewModel: AnalysisViewModel) => {
setViewModel({ ...viewModel, state: AnalysisState.ANALYZING });
}, []);

const setStateReady = useCallback((viewModel: AnalysisViewModel) => {
setViewModel({ ...viewModel, state: AnalysisState.READY });
}, []);

// ===== manipulate state ====================================================

const [viewModel, setViewModel] = useState<AnalysisViewModel>({
state: AnalysisState.INIT,
ta: INIT_AUTOMATON,
Expand All @@ -291,6 +303,8 @@ export function useAnalysisViewModel(): AnalysisViewModel {
addClock: addClock,
editClock: editClock,
removeClock: removeClock,
setStateAnalyzing: setStateAnalyzing,
setStateReady: setStateReady,
});

// ===================================================================================================================
Expand All @@ -304,7 +318,6 @@ export function useAnalysisViewModel(): AnalysisViewModel {

useEffect(() => {
if (viewModel.state === AnalysisState.ANALYZING) {
// TODO: analyze TA
setViewModel({ ...viewModel, state: AnalysisState.READY });
}
}, [viewModel]);
Expand Down

0 comments on commit fe6dfb1

Please sign in to comment.