mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Implement ADF Add Form and Overview
This commit is contained in:
parent
9012f0ee23
commit
a965f75e4b
@ -31,6 +31,7 @@
|
|||||||
"@fontsource/roboto": "^4.5.8",
|
"@fontsource/roboto": "^4.5.8",
|
||||||
"@mui/material": "^5.11.4",
|
"@mui/material": "^5.11.4",
|
||||||
"react": "^18.2.0",
|
"react": "^18.2.0",
|
||||||
"react-dom": "^18.2.0"
|
"react-dom": "^18.2.0",
|
||||||
|
"react-router-dom": "^6.10.0"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
78
frontend/src/components/adf-details.tsx
Normal file
78
frontend/src/components/adf-details.tsx
Normal file
@ -0,0 +1,78 @@
|
|||||||
|
import React from 'react';
|
||||||
|
|
||||||
|
import { AlertColor } from '@mui/material';
|
||||||
|
|
||||||
|
import { GraphProps } from './graph-g6';
|
||||||
|
|
||||||
|
export type Parsing = 'Naive' | 'Hybrid';
|
||||||
|
|
||||||
|
export type StrategySnakeCase = 'parse_only' | 'ground' | 'complete' | 'stable' | 'stable_counting_a' | 'stable_counting_b' | 'stable_nogood';
|
||||||
|
|
||||||
|
export type StrategyCamelCase = 'ParseOnly' | 'Ground' | 'Complete' | 'Stable' | 'StableCountingA' | 'StableCountingB' | 'StableNogood';
|
||||||
|
|
||||||
|
export interface AcAndGraph {
|
||||||
|
ac: string[],
|
||||||
|
graph: GraphProps,
|
||||||
|
}
|
||||||
|
|
||||||
|
export type AcsWithGraphsOpt = {
|
||||||
|
type: 'None',
|
||||||
|
} | {
|
||||||
|
type: 'Error',
|
||||||
|
content: string
|
||||||
|
} | {
|
||||||
|
type: 'Some',
|
||||||
|
content: AcAndGraph[]
|
||||||
|
};
|
||||||
|
|
||||||
|
export type Task = {
|
||||||
|
type: 'Parse',
|
||||||
|
} | {
|
||||||
|
type: 'Solve',
|
||||||
|
content: StrategyCamelCase,
|
||||||
|
};
|
||||||
|
|
||||||
|
export interface AdfProblemInfo {
|
||||||
|
name: string,
|
||||||
|
code: string,
|
||||||
|
parsing_used: Parsing,
|
||||||
|
// NOTE: the keys are really only strategies
|
||||||
|
acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt },
|
||||||
|
running_tasks: Task[],
|
||||||
|
}
|
||||||
|
|
||||||
|
export function acsWithGraphOptToColor(status: AcsWithGraphsOpt, running: boolean): AlertColor {
|
||||||
|
if (running) {
|
||||||
|
return 'warning';
|
||||||
|
}
|
||||||
|
|
||||||
|
switch (status.type) {
|
||||||
|
case 'None': return 'info';
|
||||||
|
case 'Error': return 'error';
|
||||||
|
case 'Some': return 'success';
|
||||||
|
default:
|
||||||
|
throw new Error('Unknown type union variant (cannot occur)');
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
export function acsWithGraphOptToText(status: AcsWithGraphsOpt, running: boolean): string {
|
||||||
|
if (running) {
|
||||||
|
return 'Running';
|
||||||
|
}
|
||||||
|
|
||||||
|
switch (status.type) {
|
||||||
|
case 'None': return 'Not attempted';
|
||||||
|
case 'Error': return 'Failed';
|
||||||
|
case 'Some': return 'Done';
|
||||||
|
default:
|
||||||
|
throw new Error('Unknown type union variant (cannot occur)');
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
function AdfDetails() {
|
||||||
|
return (
|
||||||
|
<div>Details</div>
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
export default AdfDetails;
|
||||||
168
frontend/src/components/adf-new-form.tsx
Normal file
168
frontend/src/components/adf-new-form.tsx
Normal file
@ -0,0 +1,168 @@
|
|||||||
|
import React, {
|
||||||
|
useState, useContext, useCallback, useRef,
|
||||||
|
} from 'react';
|
||||||
|
|
||||||
|
import {
|
||||||
|
Button,
|
||||||
|
Container,
|
||||||
|
FormControl,
|
||||||
|
FormControlLabel,
|
||||||
|
FormLabel,
|
||||||
|
Link,
|
||||||
|
Paper,
|
||||||
|
Radio,
|
||||||
|
RadioGroup,
|
||||||
|
Stack,
|
||||||
|
Typography,
|
||||||
|
TextField,
|
||||||
|
ToggleButtonGroup,
|
||||||
|
ToggleButton,
|
||||||
|
} from '@mui/material';
|
||||||
|
|
||||||
|
import LoadingContext from './loading-context';
|
||||||
|
import SnackbarContext from './snackbar-context';
|
||||||
|
|
||||||
|
import { Parsing } from './adf-details';
|
||||||
|
|
||||||
|
const PLACEHOLDER = `s(a).
|
||||||
|
s(b).
|
||||||
|
s(c).
|
||||||
|
s(d).
|
||||||
|
ac(a,c(v)).
|
||||||
|
ac(b,b).
|
||||||
|
ac(c,and(a,b)).
|
||||||
|
ac(d,neg(b)).`;
|
||||||
|
|
||||||
|
function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
||||||
|
const { setLoading } = useContext(LoadingContext);
|
||||||
|
const { setStatus: setSnackbarInfo } = useContext(SnackbarContext);
|
||||||
|
const [isFileUpload, setFileUpload] = useState(false);
|
||||||
|
const [code, setCode] = useState(PLACEHOLDER);
|
||||||
|
const [filename, setFilename] = useState('');
|
||||||
|
const [parsing, setParsing] = useState<Parsing>('Naive');
|
||||||
|
const [name, setName] = useState('');
|
||||||
|
const fileRef = useRef<HTMLInputElement>(null);
|
||||||
|
|
||||||
|
const addAdf = useCallback(
|
||||||
|
() => {
|
||||||
|
setLoading(true);
|
||||||
|
|
||||||
|
const formData = new FormData();
|
||||||
|
|
||||||
|
if (isFileUpload && fileRef.current) {
|
||||||
|
const file = fileRef.current.files?.[0];
|
||||||
|
if (file) {
|
||||||
|
formData.append('file', file);
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
formData.append('code', code);
|
||||||
|
}
|
||||||
|
|
||||||
|
formData.append('parsing', parsing);
|
||||||
|
formData.append('name', name);
|
||||||
|
|
||||||
|
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/add`, {
|
||||||
|
method: 'POST',
|
||||||
|
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
|
||||||
|
body: formData,
|
||||||
|
})
|
||||||
|
.then((res) => {
|
||||||
|
switch (res.status) {
|
||||||
|
case 200:
|
||||||
|
setSnackbarInfo({ message: 'Successfully added ADF problem!', severity: 'success', potentialUserChange: true });
|
||||||
|
fetchProblems();
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
setSnackbarInfo({ message: 'An error occured while adding the ADF problem.', severity: 'error', potentialUserChange: true });
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
})
|
||||||
|
.finally(() => setLoading(false));
|
||||||
|
},
|
||||||
|
[isFileUpload, code, filename, parsing, name, fileRef.current],
|
||||||
|
);
|
||||||
|
|
||||||
|
return (
|
||||||
|
<Container>
|
||||||
|
<Paper elevation={8} sx={{ padding: 2 }}>
|
||||||
|
<Typography variant="h4" component="h2" align="center" gutterBottom>
|
||||||
|
Add a new Problem
|
||||||
|
</Typography>
|
||||||
|
<Container sx={{ marginTop: 2, marginBottom: 2 }}>
|
||||||
|
<Stack direction="row" justifyContent="center">
|
||||||
|
<ToggleButtonGroup
|
||||||
|
value={isFileUpload}
|
||||||
|
exclusive
|
||||||
|
onChange={(_e, newValue) => { setFileUpload(newValue); setFilename(''); }}
|
||||||
|
>
|
||||||
|
<ToggleButton value={false}>
|
||||||
|
Write by Hand
|
||||||
|
</ToggleButton>
|
||||||
|
<ToggleButton value>
|
||||||
|
Upload File
|
||||||
|
</ToggleButton>
|
||||||
|
</ToggleButtonGroup>
|
||||||
|
</Stack>
|
||||||
|
</Container>
|
||||||
|
|
||||||
|
<Container sx={{ marginTop: 2, marginBottom: 2 }}>
|
||||||
|
{isFileUpload ? (
|
||||||
|
<Stack direction="row" justifyContent="center">
|
||||||
|
<Button component="label">
|
||||||
|
{(!!filename && fileRef?.current?.files?.[0]) ? `File '${filename.split(/[\\/]/).pop()}' selected! (Click to change)` : 'Upload File'}
|
||||||
|
<input hidden type="file" onChange={(event) => { setFilename(event.target.value); }} ref={fileRef} />
|
||||||
|
</Button>
|
||||||
|
</Stack>
|
||||||
|
) : (
|
||||||
|
<TextField
|
||||||
|
name="code"
|
||||||
|
label="Put your code here:"
|
||||||
|
helperText={(
|
||||||
|
<>
|
||||||
|
For more info on the syntax, have a
|
||||||
|
look
|
||||||
|
{' '}
|
||||||
|
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
|
||||||
|
.
|
||||||
|
</>
|
||||||
|
)}
|
||||||
|
multiline
|
||||||
|
fullWidth
|
||||||
|
variant="filled"
|
||||||
|
value={code}
|
||||||
|
onChange={(event) => { setCode(event.target.value); }}
|
||||||
|
/>
|
||||||
|
)}
|
||||||
|
</Container>
|
||||||
|
|
||||||
|
<Container sx={{ marginTop: 2 }}>
|
||||||
|
<Stack direction="row" justifyContent="center" spacing={2}>
|
||||||
|
<FormControl>
|
||||||
|
<FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
|
||||||
|
<RadioGroup
|
||||||
|
row
|
||||||
|
aria-labelledby="parsing-radio-group"
|
||||||
|
name="parsing"
|
||||||
|
value={parsing}
|
||||||
|
onChange={(e) => setParsing(((e.target as HTMLInputElement).value) as Parsing)}
|
||||||
|
>
|
||||||
|
<FormControlLabel value="Naive" control={<Radio />} label="Naive" />
|
||||||
|
<FormControlLabel value="Hybrid" control={<Radio />} label="Hybrid" />
|
||||||
|
</RadioGroup>
|
||||||
|
</FormControl>
|
||||||
|
<TextField
|
||||||
|
name="name"
|
||||||
|
label="Adf Problem Name (optional):"
|
||||||
|
variant="standard"
|
||||||
|
value={name}
|
||||||
|
onChange={(event) => { setName(event.target.value); }}
|
||||||
|
/>
|
||||||
|
<Button variant="outlined" onClick={() => addAdf()}>Add Adf Problem</Button>
|
||||||
|
</Stack>
|
||||||
|
</Container>
|
||||||
|
</Paper>
|
||||||
|
</Container>
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
export default AdfNewForm;
|
||||||
164
frontend/src/components/adf-overview.tsx
Normal file
164
frontend/src/components/adf-overview.tsx
Normal file
@ -0,0 +1,164 @@
|
|||||||
|
import React, {
|
||||||
|
useRef, useState, useCallback, useEffect, useContext,
|
||||||
|
} from 'react';
|
||||||
|
|
||||||
|
import {
|
||||||
|
Chip,
|
||||||
|
Container,
|
||||||
|
Paper,
|
||||||
|
TableContainer,
|
||||||
|
Table,
|
||||||
|
TableHead,
|
||||||
|
TableRow,
|
||||||
|
TableCell,
|
||||||
|
TableBody,
|
||||||
|
Typography,
|
||||||
|
} from '@mui/material';
|
||||||
|
|
||||||
|
import AdfNewForm from './adf-new-form';
|
||||||
|
|
||||||
|
import {
|
||||||
|
AdfProblemInfo,
|
||||||
|
StrategySnakeCase,
|
||||||
|
StrategyCamelCase,
|
||||||
|
Task,
|
||||||
|
acsWithGraphOptToColor,
|
||||||
|
acsWithGraphOptToText,
|
||||||
|
} from './adf-details';
|
||||||
|
|
||||||
|
import SnackbarContext from './snackbar-context';
|
||||||
|
|
||||||
|
function AdfOverview() {
|
||||||
|
const { status: snackbarInfo } = useContext(SnackbarContext);
|
||||||
|
const [problems, setProblems] = useState<AdfProblemInfo[]>([]);
|
||||||
|
|
||||||
|
const isFirstRender = useRef(true);
|
||||||
|
|
||||||
|
const fetchProblems = useCallback(
|
||||||
|
() => {
|
||||||
|
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/`, {
|
||||||
|
method: 'GET',
|
||||||
|
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
|
||||||
|
headers: {
|
||||||
|
'Content-Type': 'application/json',
|
||||||
|
},
|
||||||
|
})
|
||||||
|
.then((res) => {
|
||||||
|
switch (res.status) {
|
||||||
|
case 200:
|
||||||
|
res.json().then((resProblems) => {
|
||||||
|
setProblems(resProblems);
|
||||||
|
});
|
||||||
|
break;
|
||||||
|
case 401:
|
||||||
|
setProblems([]);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
});
|
||||||
|
},
|
||||||
|
[setProblems],
|
||||||
|
);
|
||||||
|
|
||||||
|
useEffect(
|
||||||
|
() => {
|
||||||
|
// TODO: having the info if the user may have changed on the snackbar info
|
||||||
|
// is a bit lazy and unclean; be better!
|
||||||
|
if (isFirstRender.current || snackbarInfo?.potentialUserChange) {
|
||||||
|
isFirstRender.current = false;
|
||||||
|
|
||||||
|
fetchProblems();
|
||||||
|
}
|
||||||
|
},
|
||||||
|
[snackbarInfo?.potentialUserChange],
|
||||||
|
);
|
||||||
|
|
||||||
|
useEffect(
|
||||||
|
() => {
|
||||||
|
// if there is a running task, fetch problems again after 20 seconds
|
||||||
|
let timeout: ReturnType<typeof setTimeout>;
|
||||||
|
if (problems.some((p) => p.running_tasks.length > 0)) {
|
||||||
|
timeout = setTimeout(() => fetchProblems(), 20000);
|
||||||
|
}
|
||||||
|
|
||||||
|
return () => {
|
||||||
|
if (timeout) {
|
||||||
|
clearTimeout(timeout);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
},
|
||||||
|
[problems],
|
||||||
|
);
|
||||||
|
|
||||||
|
return (
|
||||||
|
<>
|
||||||
|
<Typography variant="h3" component="h1" align="center" gutterBottom>
|
||||||
|
ADF-BDD.DEV
|
||||||
|
</Typography>
|
||||||
|
{problems.length > 0
|
||||||
|
&& (
|
||||||
|
<Container sx={{ marginBottom: 4 }}>
|
||||||
|
<Paper elevation={8} sx={{ padding: 2 }}>
|
||||||
|
<Typography variant="h4" component="h2" align="center" gutterBottom>
|
||||||
|
Existing Problems
|
||||||
|
</Typography>
|
||||||
|
<TableContainer component={Paper}>
|
||||||
|
<Table>
|
||||||
|
<TableHead>
|
||||||
|
<TableRow>
|
||||||
|
<TableCell align="center">ADF Problem Name</TableCell>
|
||||||
|
<TableCell align="center">Parse Status</TableCell>
|
||||||
|
<TableCell align="center">Grounded Solution</TableCell>
|
||||||
|
<TableCell align="center">Complete Solution</TableCell>
|
||||||
|
<TableCell align="center">Stable Solution</TableCell>
|
||||||
|
<TableCell align="center">Stable Solution (Counting Method A)</TableCell>
|
||||||
|
<TableCell align="center">Stable Solution (Counting Method B)</TableCell>
|
||||||
|
<TableCell align="center">Stable Solution (Nogood-Based)</TableCell>
|
||||||
|
</TableRow>
|
||||||
|
</TableHead>
|
||||||
|
<TableBody>
|
||||||
|
{problems.map((problem) => (
|
||||||
|
<TableRow
|
||||||
|
key={problem.name}
|
||||||
|
sx={{ '&:last-child td, &:last-child th': { border: 0 } }}
|
||||||
|
>
|
||||||
|
<TableCell component="th" scope="row">
|
||||||
|
{problem.name}
|
||||||
|
</TableCell>
|
||||||
|
{
|
||||||
|
(() => {
|
||||||
|
const status = problem.acs_per_strategy.parse_only;
|
||||||
|
const running = problem.running_tasks.some((t: Task) => t.type === 'Parse');
|
||||||
|
|
||||||
|
const color = acsWithGraphOptToColor(status, running);
|
||||||
|
const text = acsWithGraphOptToText(status, running);
|
||||||
|
|
||||||
|
return <TableCell align="center"><Chip color={color} label={`${text} (${problem.parsing_used} Parsing)`} /></TableCell>;
|
||||||
|
})()
|
||||||
|
}
|
||||||
|
{
|
||||||
|
(['Ground', 'Complete', 'Stable', 'StableCountingA', 'StableCountingB', 'StableNogood'] as StrategyCamelCase[]).map((strategy) => {
|
||||||
|
const status = problem.acs_per_strategy[strategy.replace(/^([A-Z])/, (_, p1) => p1.toLowerCase()).replace(/([A-Z])/g, (_, p1) => `_${p1.toLowerCase()}`) as StrategySnakeCase];
|
||||||
|
const running = problem.running_tasks.some((t: Task) => t.type === 'Solve' && t.content === strategy);
|
||||||
|
|
||||||
|
const color = acsWithGraphOptToColor(status, running);
|
||||||
|
const text = acsWithGraphOptToText(status, running);
|
||||||
|
|
||||||
|
return <TableCell key={strategy} align="center"><Chip color={color} label={text} /></TableCell>;
|
||||||
|
})
|
||||||
|
}
|
||||||
|
</TableRow>
|
||||||
|
))}
|
||||||
|
</TableBody>
|
||||||
|
</Table>
|
||||||
|
</TableContainer>
|
||||||
|
</Paper>
|
||||||
|
</Container>
|
||||||
|
)}
|
||||||
|
<AdfNewForm fetchProblems={fetchProblems} />
|
||||||
|
</>
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
export default AdfOverview;
|
||||||
@ -1,180 +1,83 @@
|
|||||||
import * as React from 'react';
|
import React, { useState, useMemo } from 'react';
|
||||||
|
|
||||||
|
import { createBrowserRouter, RouterProvider } from 'react-router-dom';
|
||||||
|
|
||||||
import { ThemeProvider, createTheme } from '@mui/material/styles';
|
import { ThemeProvider, createTheme } from '@mui/material/styles';
|
||||||
import {
|
import {
|
||||||
|
Alert,
|
||||||
|
AlertColor,
|
||||||
Backdrop,
|
Backdrop,
|
||||||
Button,
|
|
||||||
CircularProgress,
|
CircularProgress,
|
||||||
CssBaseline,
|
CssBaseline,
|
||||||
Container,
|
Snackbar,
|
||||||
FormControl,
|
useMediaQuery,
|
||||||
FormControlLabel,
|
|
||||||
FormLabel,
|
|
||||||
Link,
|
|
||||||
Pagination,
|
|
||||||
Paper,
|
|
||||||
Radio,
|
|
||||||
RadioGroup,
|
|
||||||
Typography,
|
|
||||||
TextField,
|
|
||||||
} from '@mui/material';
|
} from '@mui/material';
|
||||||
|
|
||||||
import LoadingContext from './loading-context';
|
import LoadingContext from './loading-context';
|
||||||
import GraphG6, { GraphProps } from './graph-g6';
|
import SnackbarContext from './snackbar-context';
|
||||||
import Footer from './footer';
|
import Footer from './footer';
|
||||||
|
import AdfOverview from './adf-overview';
|
||||||
|
import AdfDetails from './adf-details';
|
||||||
|
|
||||||
const { useState, useCallback, useMemo } = React;
|
const browserRouter = createBrowserRouter([
|
||||||
|
{
|
||||||
const darkTheme = createTheme({
|
path: '/',
|
||||||
palette: {
|
element: <AdfOverview />,
|
||||||
mode: 'dark',
|
|
||||||
},
|
},
|
||||||
});
|
{
|
||||||
|
path: '/:adfName',
|
||||||
const placeholder = `s(a).
|
element: <AdfDetails />,
|
||||||
s(b).
|
},
|
||||||
s(c).
|
]);
|
||||||
s(d).
|
|
||||||
ac(a,c(v)).
|
|
||||||
ac(b,b).
|
|
||||||
ac(c,and(a,b)).
|
|
||||||
ac(d,neg(b)).`;
|
|
||||||
|
|
||||||
enum Parsing {
|
|
||||||
Naive = 'Naive',
|
|
||||||
Hybrid = 'Hybrid',
|
|
||||||
}
|
|
||||||
|
|
||||||
enum Strategy {
|
|
||||||
ParseOnly = 'ParseOnly',
|
|
||||||
Ground = 'Ground',
|
|
||||||
Complete = 'Complete',
|
|
||||||
Stable = 'Stable',
|
|
||||||
StableCountingA = 'StableCountingA',
|
|
||||||
StableCountingB = 'StableCountingB',
|
|
||||||
StableNogood = 'StableNogood',
|
|
||||||
}
|
|
||||||
|
|
||||||
function App() {
|
function App() {
|
||||||
const [loading, setLoading] = useState(false);
|
const prefersDarkMode = useMediaQuery('(prefers-color-scheme: dark)');
|
||||||
const [code, setCode] = useState(placeholder);
|
|
||||||
const [parsing, setParsing] = useState(Parsing.Naive);
|
|
||||||
const [graphs, setGraphs] = useState<GraphProps[]>();
|
|
||||||
const [graphIndex, setGraphIndex] = useState(0);
|
|
||||||
|
|
||||||
const submitHandler = useCallback(
|
const theme = useMemo(
|
||||||
(strategy: Strategy) => {
|
() => createTheme({
|
||||||
setLoading(true);
|
palette: {
|
||||||
|
mode: prefersDarkMode ? 'dark' : 'light',
|
||||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
|
},
|
||||||
method: 'POST',
|
}),
|
||||||
headers: {
|
[prefersDarkMode],
|
||||||
'Content-Type': 'application/json',
|
|
||||||
},
|
|
||||||
body: JSON.stringify({ code, strategy, parsing }),
|
|
||||||
})
|
|
||||||
.then((res) => res.json())
|
|
||||||
.then((data) => {
|
|
||||||
setGraphs(data);
|
|
||||||
setGraphIndex(0);
|
|
||||||
})
|
|
||||||
.finally(() => setLoading(false));
|
|
||||||
// TODO: error handling
|
|
||||||
},
|
|
||||||
[code, parsing],
|
|
||||||
);
|
);
|
||||||
|
|
||||||
|
const [loading, setLoading] = useState(false);
|
||||||
const loadingContext = useMemo(() => ({ loading, setLoading }), [loading, setLoading]);
|
const loadingContext = useMemo(() => ({ loading, setLoading }), [loading, setLoading]);
|
||||||
|
|
||||||
|
const [snackbarInfo, setSnackbarInfo] = useState<{
|
||||||
|
message: string,
|
||||||
|
severity: AlertColor,
|
||||||
|
potentialUserChange: boolean,
|
||||||
|
} | undefined>();
|
||||||
|
const snackbarContext = useMemo(
|
||||||
|
() => ({ status: snackbarInfo, setStatus: setSnackbarInfo }),
|
||||||
|
[snackbarInfo, setSnackbarInfo],
|
||||||
|
);
|
||||||
|
|
||||||
return (
|
return (
|
||||||
<ThemeProvider theme={darkTheme}>
|
<ThemeProvider theme={theme}>
|
||||||
<LoadingContext.Provider value={loadingContext}>
|
<LoadingContext.Provider value={loadingContext}>
|
||||||
<CssBaseline />
|
<SnackbarContext.Provider value={snackbarContext}>
|
||||||
<main>
|
<CssBaseline />
|
||||||
<Typography variant="h2" component="h1" align="center" gutterBottom>
|
<main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
|
||||||
Solve your ADF Problem with OBDDs!
|
<RouterProvider router={browserRouter} />
|
||||||
</Typography>
|
</main>
|
||||||
|
<Footer />
|
||||||
|
|
||||||
<Container>
|
<Backdrop
|
||||||
<TextField
|
open={loading}
|
||||||
name="code"
|
>
|
||||||
label="Put your code here:"
|
<CircularProgress color="inherit" />
|
||||||
helperText={(
|
</Backdrop>
|
||||||
<>
|
<Snackbar
|
||||||
For more info on the syntax, have a
|
open={!!snackbarInfo}
|
||||||
look
|
autoHideDuration={10000}
|
||||||
{' '}
|
onClose={() => setSnackbarInfo(undefined)}
|
||||||
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
|
>
|
||||||
.
|
<Alert severity={snackbarInfo?.severity}>{snackbarInfo?.message}</Alert>
|
||||||
</>
|
</Snackbar>
|
||||||
)}
|
</SnackbarContext.Provider>
|
||||||
multiline
|
|
||||||
fullWidth
|
|
||||||
variant="filled"
|
|
||||||
value={code}
|
|
||||||
onChange={(event) => { setCode(event.target.value); }}
|
|
||||||
/>
|
|
||||||
</Container>
|
|
||||||
<Container sx={{ marginTop: 2, marginBottom: 2 }}>
|
|
||||||
<FormControl>
|
|
||||||
<FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
|
|
||||||
<RadioGroup
|
|
||||||
row
|
|
||||||
aria-labelledby="parsing-radio-group"
|
|
||||||
name="parsing"
|
|
||||||
value={parsing}
|
|
||||||
onChange={(e) => setParsing(((e.target as HTMLInputElement).value) as Parsing)}
|
|
||||||
>
|
|
||||||
<FormControlLabel value={Parsing.Naive} control={<Radio />} label="Naive" />
|
|
||||||
<FormControlLabel value={Parsing.Hybrid} control={<Radio />} label="Hybrid" />
|
|
||||||
</RadioGroup>
|
|
||||||
</FormControl>
|
|
||||||
<br />
|
|
||||||
<br />
|
|
||||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.ParseOnly)}>Parse only</Button>
|
|
||||||
{' '}
|
|
||||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.Ground)}>Grounded Model</Button>
|
|
||||||
{' '}
|
|
||||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.Complete)}>Complete Models</Button>
|
|
||||||
{' '}
|
|
||||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.Stable)}>Stable Models (naive heuristics)</Button>
|
|
||||||
{' '}
|
|
||||||
<Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingA)}>Stable Models (counting heuristic A)</Button>
|
|
||||||
{' '}
|
|
||||||
<Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingB)}>Stable Models (counting heuristic B)</Button>
|
|
||||||
{' '}
|
|
||||||
<Button variant="outlined" onClick={() => submitHandler(Strategy.StableNogood)}>Stable Models using nogoods (Simple Heuristic)</Button>
|
|
||||||
</Container>
|
|
||||||
|
|
||||||
{graphs
|
|
||||||
&& (
|
|
||||||
<Container sx={{ marginTop: 4, marginBottom: 4 }}>
|
|
||||||
{graphs.length > 1
|
|
||||||
&& (
|
|
||||||
<>
|
|
||||||
Models:
|
|
||||||
<br />
|
|
||||||
<Pagination variant="outlined" shape="rounded" count={graphs.length} page={graphIndex + 1} onChange={(e, value) => setGraphIndex(value - 1)} />
|
|
||||||
</>
|
|
||||||
)}
|
|
||||||
{graphs.length > 0
|
|
||||||
&& (
|
|
||||||
<Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
|
|
||||||
<GraphG6 graph={graphs[graphIndex]} />
|
|
||||||
</Paper>
|
|
||||||
)}
|
|
||||||
{graphs.length === 0
|
|
||||||
&& <>No models!</>}
|
|
||||||
</Container>
|
|
||||||
)}
|
|
||||||
</main>
|
|
||||||
<Footer />
|
|
||||||
|
|
||||||
<Backdrop
|
|
||||||
open={loading}
|
|
||||||
>
|
|
||||||
<CircularProgress color="inherit" />
|
|
||||||
</Backdrop>
|
|
||||||
</LoadingContext.Provider>
|
</LoadingContext.Provider>
|
||||||
</ThemeProvider>
|
</ThemeProvider>
|
||||||
);
|
);
|
||||||
|
|||||||
@ -1,5 +1,5 @@
|
|||||||
import React, {
|
import React, {
|
||||||
useState, useCallback, useContext, useEffect,
|
useState, useCallback, useContext, useEffect, useRef,
|
||||||
} from 'react';
|
} from 'react';
|
||||||
|
|
||||||
import {
|
import {
|
||||||
@ -11,12 +11,12 @@ import {
|
|||||||
DialogActions,
|
DialogActions,
|
||||||
DialogContent,
|
DialogContent,
|
||||||
DialogTitle,
|
DialogTitle,
|
||||||
Snackbar,
|
|
||||||
TextField,
|
TextField,
|
||||||
Toolbar,
|
Toolbar,
|
||||||
} from '@mui/material';
|
} from '@mui/material';
|
||||||
|
|
||||||
import LoadingContext from './loading-context';
|
import LoadingContext from './loading-context';
|
||||||
|
import SnackbarContext from './snackbar-context';
|
||||||
|
|
||||||
enum UserFormType {
|
enum UserFormType {
|
||||||
Login = 'Login',
|
Login = 'Login',
|
||||||
@ -77,7 +77,7 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
|
|||||||
.then((res) => {
|
.then((res) => {
|
||||||
switch (res.status) {
|
switch (res.status) {
|
||||||
case 200:
|
case 200:
|
||||||
close(`Action '${formType}' successful!`, 'success');
|
close(`Action '${del ? 'Delete' : formType}' successful!`, 'success');
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
setError(true);
|
setError(true);
|
||||||
@ -113,13 +113,14 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
|
|||||||
</DialogContent>
|
</DialogContent>
|
||||||
<DialogActions>
|
<DialogActions>
|
||||||
<Button type="button" onClick={() => close()}>Cancel</Button>
|
<Button type="button" onClick={() => close()}>Cancel</Button>
|
||||||
<Button type="submit">{formType}</Button>
|
<Button type="submit" variant="contained" color="success">{formType}</Button>
|
||||||
{formType === UserFormType.Update
|
{formType === UserFormType.Update
|
||||||
// TODO: add another confirm dialog here
|
// TODO: add another confirm dialog here
|
||||||
&& (
|
&& (
|
||||||
<Button
|
<Button
|
||||||
type="button"
|
type="button"
|
||||||
variant="outlined"
|
variant="outlined"
|
||||||
|
color="error"
|
||||||
onClick={() => {
|
onClick={() => {
|
||||||
// eslint-disable-next-line no-alert
|
// eslint-disable-next-line no-alert
|
||||||
if (window.confirm('Are you sure that you want to delete your account?')) {
|
if (window.confirm('Are you sure that you want to delete your account?')) {
|
||||||
@ -138,13 +139,12 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
|
|||||||
UserForm.defaultProps = { username: undefined };
|
UserForm.defaultProps = { username: undefined };
|
||||||
|
|
||||||
function Footer() {
|
function Footer() {
|
||||||
|
const { status: snackbarInfo, setStatus: setSnackbarInfo } = useContext(SnackbarContext);
|
||||||
const [username, setUsername] = useState<string>();
|
const [username, setUsername] = useState<string>();
|
||||||
const [tempUser, setTempUser] = useState<boolean>();
|
const [tempUser, setTempUser] = useState<boolean>();
|
||||||
const [dialogTypeOpen, setDialogTypeOpen] = useState<UserFormType | null>(null);
|
const [dialogTypeOpen, setDialogTypeOpen] = useState<UserFormType | null>(null);
|
||||||
const [snackbarInfo, setSnackbarInfo] = useState<{
|
|
||||||
message: string,
|
const isFirstRender = useRef(true);
|
||||||
severity: AlertColor,
|
|
||||||
} | undefined>();
|
|
||||||
|
|
||||||
const logout = useCallback(() => {
|
const logout = useCallback(() => {
|
||||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/logout`, {
|
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/logout`, {
|
||||||
@ -157,19 +157,22 @@ function Footer() {
|
|||||||
.then((res) => {
|
.then((res) => {
|
||||||
switch (res.status) {
|
switch (res.status) {
|
||||||
case 200:
|
case 200:
|
||||||
setSnackbarInfo({ message: 'Logout successful!', severity: 'success' });
|
setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: true });
|
||||||
setUsername(undefined);
|
setUsername(undefined);
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
setSnackbarInfo({ message: 'An error occurred while trying to log out.', severity: 'error' });
|
setSnackbarInfo({ message: 'An error occurred while trying to log out.', severity: 'error', potentialUserChange: false });
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
}, [setSnackbarInfo]);
|
}, [setSnackbarInfo]);
|
||||||
|
|
||||||
useEffect(() => {
|
useEffect(() => {
|
||||||
// Intuition: If the dialog was just closed (or on first render).
|
// TODO: having the info if the user may have changed on the snackbar info
|
||||||
if (!dialogTypeOpen) {
|
// is a bit lazy and unclean; be better!
|
||||||
|
if (isFirstRender.current || snackbarInfo?.potentialUserChange) {
|
||||||
|
isFirstRender.current = false;
|
||||||
|
|
||||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/info`, {
|
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/info`, {
|
||||||
method: 'GET',
|
method: 'GET',
|
||||||
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
|
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
|
||||||
@ -191,7 +194,7 @@ function Footer() {
|
|||||||
}
|
}
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
}, [dialogTypeOpen]);
|
}, [snackbarInfo?.potentialUserChange]);
|
||||||
|
|
||||||
return (
|
return (
|
||||||
<>
|
<>
|
||||||
@ -222,18 +225,13 @@ function Footer() {
|
|||||||
formType={dialogTypeOpen}
|
formType={dialogTypeOpen}
|
||||||
close={(message, severity) => {
|
close={(message, severity) => {
|
||||||
setDialogTypeOpen(null);
|
setDialogTypeOpen(null);
|
||||||
setSnackbarInfo((!!message && !!severity) ? { message, severity } : undefined);
|
setSnackbarInfo((!!message && !!severity)
|
||||||
|
? { message, severity, potentialUserChange: true }
|
||||||
|
: undefined);
|
||||||
}}
|
}}
|
||||||
username={dialogTypeOpen === UserFormType.Update ? username : undefined}
|
username={dialogTypeOpen === UserFormType.Update ? username : undefined}
|
||||||
/>
|
/>
|
||||||
</Dialog>
|
</Dialog>
|
||||||
<Snackbar
|
|
||||||
open={!!snackbarInfo}
|
|
||||||
autoHideDuration={10000}
|
|
||||||
onClose={() => setSnackbarInfo(undefined)}
|
|
||||||
>
|
|
||||||
<Alert severity={snackbarInfo?.severity}>{snackbarInfo?.message}</Alert>
|
|
||||||
</Snackbar>
|
|
||||||
</>
|
</>
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|||||||
17
frontend/src/components/snackbar-context.ts
Normal file
17
frontend/src/components/snackbar-context.ts
Normal file
@ -0,0 +1,17 @@
|
|||||||
|
import { createContext } from 'react';
|
||||||
|
|
||||||
|
import { AlertColor } from '@mui/material';
|
||||||
|
|
||||||
|
type Status = { message: string, severity: AlertColor, potentialUserChange: boolean } | undefined;
|
||||||
|
|
||||||
|
interface ISnackbarContext {
|
||||||
|
status: Status;
|
||||||
|
setStatus: (status: Status) => void;
|
||||||
|
}
|
||||||
|
|
||||||
|
const SnackbarContext = createContext<ISnackbarContext>({
|
||||||
|
status: undefined,
|
||||||
|
setStatus: () => {},
|
||||||
|
});
|
||||||
|
|
||||||
|
export default SnackbarContext;
|
||||||
@ -1296,6 +1296,11 @@
|
|||||||
dependencies:
|
dependencies:
|
||||||
"@babel/runtime" "^7.0.0"
|
"@babel/runtime" "^7.0.0"
|
||||||
|
|
||||||
|
"@remix-run/router@1.5.0":
|
||||||
|
version "1.5.0"
|
||||||
|
resolved "https://registry.yarnpkg.com/@remix-run/router/-/router-1.5.0.tgz#57618e57942a5f0131374a9fdb0167e25a117fdc"
|
||||||
|
integrity sha512-bkUDCp8o1MvFO+qxkODcbhSqRa6P2GXgrGZVpt0dCXNW2HCSCqYI0ZoAqEOSAjRWmmlKcYgFvN4B4S+zo/f8kg==
|
||||||
|
|
||||||
"@swc/helpers@^0.4.12":
|
"@swc/helpers@^0.4.12":
|
||||||
version "0.4.14"
|
version "0.4.14"
|
||||||
resolved "https://registry.yarnpkg.com/@swc/helpers/-/helpers-0.4.14.tgz#1352ac6d95e3617ccb7c1498ff019654f1e12a74"
|
resolved "https://registry.yarnpkg.com/@swc/helpers/-/helpers-0.4.14.tgz#1352ac6d95e3617ccb7c1498ff019654f1e12a74"
|
||||||
@ -3615,6 +3620,21 @@ react-refresh@^0.9.0:
|
|||||||
resolved "https://registry.yarnpkg.com/react-refresh/-/react-refresh-0.9.0.tgz#71863337adc3e5c2f8a6bfddd12ae3bfe32aafbf"
|
resolved "https://registry.yarnpkg.com/react-refresh/-/react-refresh-0.9.0.tgz#71863337adc3e5c2f8a6bfddd12ae3bfe32aafbf"
|
||||||
integrity sha512-Gvzk7OZpiqKSkxsQvO/mbTN1poglhmAV7gR/DdIrRrSMXraRQQlfikRJOr3Nb9GTMPC5kof948Zy6jJZIFtDvQ==
|
integrity sha512-Gvzk7OZpiqKSkxsQvO/mbTN1poglhmAV7gR/DdIrRrSMXraRQQlfikRJOr3Nb9GTMPC5kof948Zy6jJZIFtDvQ==
|
||||||
|
|
||||||
|
react-router-dom@^6.10.0:
|
||||||
|
version "6.10.0"
|
||||||
|
resolved "https://registry.yarnpkg.com/react-router-dom/-/react-router-dom-6.10.0.tgz#090ddc5c84dc41b583ce08468c4007c84245f61f"
|
||||||
|
integrity sha512-E5dfxRPuXKJqzwSe/qGcqdwa18QiWC6f3H3cWXM24qj4N0/beCIf/CWTipop2xm7mR0RCS99NnaqPNjHtrAzCg==
|
||||||
|
dependencies:
|
||||||
|
"@remix-run/router" "1.5.0"
|
||||||
|
react-router "6.10.0"
|
||||||
|
|
||||||
|
react-router@6.10.0:
|
||||||
|
version "6.10.0"
|
||||||
|
resolved "https://registry.yarnpkg.com/react-router/-/react-router-6.10.0.tgz#230f824fde9dd0270781b5cb497912de32c0a971"
|
||||||
|
integrity sha512-Nrg0BWpQqrC3ZFFkyewrflCud9dio9ME3ojHCF/WLsprJVzkq3q3UeEhMCAW1dobjeGbWgjNn/PVF6m46ANxXQ==
|
||||||
|
dependencies:
|
||||||
|
"@remix-run/router" "1.5.0"
|
||||||
|
|
||||||
react-transition-group@^4.4.5:
|
react-transition-group@^4.4.5:
|
||||||
version "4.4.5"
|
version "4.4.5"
|
||||||
resolved "https://registry.yarnpkg.com/react-transition-group/-/react-transition-group-4.4.5.tgz#e53d4e3f3344da8521489fbef8f2581d42becdd1"
|
resolved "https://registry.yarnpkg.com/react-transition-group/-/react-transition-group-4.4.5.tgz#e53d4e3f3344da8521489fbef8f2581d42becdd1"
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user