1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

WIP: build frontend for ADFs

This commit is contained in:
monsterkrampe 2023-04-13 16:34:29 +02:00
parent da8e79147b
commit 7b6f98c934
No known key found for this signature in database
GPG Key ID: B8ADC1F5A5CE5057
13 changed files with 802 additions and 237 deletions

97
Cargo.lock generated
View File

@ -122,6 +122,44 @@ dependencies = [
"syn 1.0.109",
]
[[package]]
name = "actix-multipart"
version = "0.6.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dee489e3c01eae4d1c35b03c4493f71cb40d93f66b14558feb1b1a807671cc4e"
dependencies = [
"actix-multipart-derive",
"actix-utils",
"actix-web",
"bytes",
"derive_more",
"futures-core",
"futures-util",
"httparse",
"local-waker",
"log",
"memchr",
"mime",
"serde",
"serde_json",
"serde_plain",
"tempfile",
"tokio",
]
[[package]]
name = "actix-multipart-derive"
version = "0.6.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2ec592f234db8a253cf80531246a4407c8a70530423eea80688a6c5a44a110e7"
dependencies = [
"darling 0.14.4",
"parse-size",
"proc-macro2",
"quote",
"syn 1.0.109",
]
[[package]]
name = "actix-router"
version = "0.5.1"
@ -278,6 +316,7 @@ dependencies = [
"actix-cors",
"actix-files",
"actix-identity",
"actix-multipart",
"actix-session",
"actix-web",
"adf_bdd",
@ -918,8 +957,18 @@ version = "0.13.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a01d95850c592940db9b8194bc39f4bc0e89dee5c4265e4b1807c34a9aba453c"
dependencies = [
"darling_core",
"darling_macro",
"darling_core 0.13.4",
"darling_macro 0.13.4",
]
[[package]]
name = "darling"
version = "0.14.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7b750cb3417fd1b327431a470f388520309479ab0bf5e323505daf0290cd3850"
dependencies = [
"darling_core 0.14.4",
"darling_macro 0.14.4",
]
[[package]]
@ -936,13 +985,38 @@ dependencies = [
"syn 1.0.109",
]
[[package]]
name = "darling_core"
version = "0.14.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "109c1ca6e6b7f82cc233a97004ea8ed7ca123a9af07a8230878fcfda9b158bf0"
dependencies = [
"fnv",
"ident_case",
"proc-macro2",
"quote",
"strsim",
"syn 1.0.109",
]
[[package]]
name = "darling_macro"
version = "0.13.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9c972679f83bdf9c42bd905396b6c3588a843a17f0f16dfcfa3e2c5d57441835"
dependencies = [
"darling_core",
"darling_core 0.13.4",
"quote",
"syn 1.0.109",
]
[[package]]
name = "darling_macro"
version = "0.14.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a4aab4dbc9f7611d8b55048a3a16d2d010c2c8334e46304b40ac1cc14bf3b48e"
dependencies = [
"darling_core 0.14.4",
"quote",
"syn 1.0.109",
]
@ -1881,6 +1955,12 @@ dependencies = [
"windows-sys 0.45.0",
]
[[package]]
name = "parse-size"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "944553dd59c802559559161f9816429058b869003836120e262e8caec061b7ae"
[[package]]
name = "password-hash"
version = "0.5.0"
@ -2339,6 +2419,15 @@ dependencies = [
"serde",
]
[[package]]
name = "serde_plain"
version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d6018081315db179d0ce57b1fe4b62a12a0028c9cf9bbef868c9cf477b3c34ae"
dependencies = [
"serde",
]
[[package]]
name = "serde_urlencoded"
version = "0.7.1"
@ -2367,7 +2456,7 @@ version = "1.5.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e182d6ec6f05393cc0e5ed1bf81ad6db3a8feedf8ee515ecdd369809bcce8082"
dependencies = [
"darling",
"darling 0.13.4",
"proc-macro2",
"quote",
"syn 1.0.109",

View File

@ -31,6 +31,7 @@
"@fontsource/roboto": "^4.5.8",
"@mui/material": "^5.11.4",
"react": "^18.2.0",
"react-dom": "^18.2.0"
"react-dom": "^18.2.0",
"react-router-dom": "^6.10.0"
}
}

View File

@ -0,0 +1,73 @@
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,
acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt }, // NOTE: the keys are really only strategies
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';
}
}
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';
}
}
function AdfDetails() {
return (
<div>Details</div>
);
}
export default AdfDetails;

View File

@ -0,0 +1,169 @@
import React, {
useState, useContext, useCallback, useRef,
} from 'react';
import {
Backdrop,
Button,
CircularProgress,
CssBaseline,
Container,
FormControl,
FormControlLabel,
FormLabel,
Link,
Pagination,
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) {
formData.append('file', fileRef.current.files![0]);
} 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;

View File

@ -0,0 +1,138 @@
import React, { useState, useCallback, useEffect } from 'react';
import {
Backdrop,
Button,
Chip,
CircularProgress,
CssBaseline,
Container,
FormControl,
FormControlLabel,
FormLabel,
Link,
Pagination,
Paper,
Radio,
RadioGroup,
Stack,
TableContainer,
Table,
TableHead,
TableRow,
TableCell,
TableBody,
Typography,
TextField,
ToggleButtonGroup,
ToggleButton,
} from '@mui/material';
import AdfNewForm from './adf-new-form';
import {AdfProblemInfo, StrategySnakeCase, StrategyCamelCase, Task, acsWithGraphOptToColor, acsWithGraphOptToText} from './adf-details';
function AdfOverview() {
const [problems, setProblems] = useState<AdfProblemInfo[]>([]);
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((problems) => {
setProblems(problems);
});
break;
default:
break;
}
});
},
[setProblems],
);
useEffect(
() => { fetchProblems(); },
[],
);
// TODO set timeout for refetching if there are running 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 align="center"><Chip color={color} label={text} /></TableCell>;
})
}
</TableRow>
))}
</TableBody>
</Table>
</TableContainer>
</Paper>
</Container>
}
<AdfNewForm fetchProblems={fetchProblems} />
</>
);
}
export default AdfOverview;

View File

@ -1,7 +1,11 @@
import * as React from 'react';
import { createBrowserRouter, RouterProvider } from 'react-router-dom';
import { ThemeProvider, createTheme } from '@mui/material/styles';
import {
Alert,
AlertColor,
Backdrop,
Button,
CircularProgress,
@ -15,169 +19,190 @@ import {
Paper,
Radio,
RadioGroup,
Snackbar,
Typography,
TextField,
useMediaQuery,
} from '@mui/material';
import LoadingContext from './loading-context';
import SnackbarContext from './snackbar-context';
import GraphG6, { GraphProps } from './graph-g6';
import Footer from './footer';
import AdfOverview from './adf-overview';
import AdfDetails from './adf-details';
const { useState, useCallback, useMemo } = React;
const darkTheme = createTheme({
palette: {
mode: 'dark',
const browserRouter = createBrowserRouter([
{
path: '/',
element: <AdfOverview />,
},
});
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)).`;
enum Parsing {
Naive = 'Naive',
Hybrid = 'Hybrid',
}
enum Strategy {
ParseOnly = 'ParseOnly',
Ground = 'Ground',
Complete = 'Complete',
Stable = 'Stable',
StableCountingA = 'StableCountingA',
StableCountingB = 'StableCountingB',
StableNogood = 'StableNogood',
}
{
path: '/:adfName',
element: <AdfDetails />,
},
]);
function App() {
const [loading, setLoading] = useState(false);
const [code, setCode] = useState(placeholder);
const [parsing, setParsing] = useState(Parsing.Naive);
const [graphs, setGraphs] = useState<GraphProps[]>();
const [graphIndex, setGraphIndex] = useState(0);
const prefersDarkMode = useMediaQuery('(prefers-color-scheme: dark)');
const submitHandler = useCallback(
(strategy: Strategy) => {
setLoading(true);
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
method: 'POST',
headers: {
'Content-Type': 'application/json',
const theme = useMemo(
() =>
createTheme({
palette: {
mode: prefersDarkMode ? 'dark' : 'light',
},
body: JSON.stringify({ code, strategy, parsing }),
})
.then((res) => res.json())
.then((data) => {
setGraphs(data);
setGraphIndex(0);
})
.finally(() => setLoading(false));
// TODO: error handling
},
[code, parsing],
}),
[prefersDarkMode],
);
const [loading, setLoading] = useState(false);
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 (
<ThemeProvider theme={darkTheme}>
<ThemeProvider theme={theme}>
<LoadingContext.Provider value={loadingContext}>
<CssBaseline />
<main>
<Typography variant="h2" component="h1" align="center" gutterBottom>
Solve your ADF Problem with OBDDs!
</Typography>
<SnackbarContext.Provider value={snackbarContext}>
<CssBaseline />
<main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
<RouterProvider router={browserRouter} />
</main>
<Footer />
<Container>
<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, 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>
<Backdrop
open={loading}
>
<CircularProgress color="inherit" />
</Backdrop>
<Snackbar
open={!!snackbarInfo}
autoHideDuration={10000}
onClose={() => setSnackbarInfo(undefined)}
>
<Alert severity={snackbarInfo?.severity}>{snackbarInfo?.message}</Alert>
</Snackbar>
</SnackbarContext.Provider>
</LoadingContext.Provider>
</ThemeProvider>
);
}
// function BACKUP() {
// const [code, setCode] = useState(placeholder);
// const [parsing, setParsing] = useState(Parsing.Naive);
// const [graphs, setGraphs] = useState<GraphProps[]>();
// const [graphIndex, setGraphIndex] = useState(0);
// const submitHandler = useCallback(
// (strategy: Strategy) => {
// setLoading(true);
// fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
// method: 'POST',
// headers: {
// '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],
// );
// return (<>
// <Typography variant="h2" component="h1" align="center" gutterBottom>
// Solve your ADF Problem with OBDDs!
// </Typography>
// <Container>
// <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, 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>
// )}
// </>
// );
// }
export default App;

View File

@ -1,5 +1,5 @@
import React, {
useState, useCallback, useContext, useEffect,
useState, useCallback, useContext, useEffect, useRef,
} from 'react';
import {
@ -17,6 +17,7 @@ import {
} from '@mui/material';
import LoadingContext from './loading-context';
import SnackbarContext from './snackbar-context';
enum UserFormType {
Login = 'Login',
@ -138,13 +139,12 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
UserForm.defaultProps = { username: undefined };
function Footer() {
const { status: snackbarInfo, setStatus: setSnackbarInfo } = useContext(SnackbarContext);
const [username, setUsername] = useState<string>();
const [tempUser, setTempUser] = useState<boolean>();
const [dialogTypeOpen, setDialogTypeOpen] = useState<UserFormType | null>(null);
const [snackbarInfo, setSnackbarInfo] = useState<{
message: string,
severity: AlertColor,
} | undefined>();
const isFirstRender = useRef(true);
const logout = useCallback(() => {
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/logout`, {
@ -157,19 +157,21 @@ function Footer() {
.then((res) => {
switch (res.status) {
case 200:
setSnackbarInfo({ message: 'Logout successful!', severity: 'success' });
setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: false });
setUsername(undefined);
break;
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;
}
});
}, [setSnackbarInfo]);
useEffect(() => {
// Intuition: If the dialog was just closed (or on first render).
if (!dialogTypeOpen) {
// 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;
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/info`, {
method: 'GET',
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
@ -191,7 +193,7 @@ function Footer() {
}
});
}
}, [dialogTypeOpen]);
}, [snackbarInfo?.potentialUserChange]);
return (
<>
@ -222,18 +224,11 @@ function Footer() {
formType={dialogTypeOpen}
close={(message, severity) => {
setDialogTypeOpen(null);
setSnackbarInfo((!!message && !!severity) ? { message, severity } : undefined);
setSnackbarInfo((!!message && !!severity) ? { message, severity, potentialUserChange: true } : undefined);
}}
username={dialogTypeOpen === UserFormType.Update ? username : undefined}
/>
</Dialog>
<Snackbar
open={!!snackbarInfo}
autoHideDuration={10000}
onClose={() => setSnackbarInfo(undefined)}
>
<Alert severity={snackbarInfo?.severity}>{snackbarInfo?.message}</Alert>
</Snackbar>
</>
);
}

View 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;

View File

@ -1296,6 +1296,11 @@
dependencies:
"@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":
version "0.4.14"
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"
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:
version "4.4.5"
resolved "https://registry.yarnpkg.com/react-transition-group/-/react-transition-group-4.4.5.tgz#e53d4e3f3344da8521489fbef8f2581d42becdd1"

View File

@ -25,6 +25,7 @@ argon2 = "0.5.0"
actix-session = { version="0.7.2", features = ["cookie-session"] }
names = "0.14.0"
futures-util = "0.3.28"
actix-multipart = "0.6.0"
[features]
cors_for_local_development = []

View File

@ -4,6 +4,7 @@ use std::sync::{Arc, RwLock};
use std::time::Duration;
use actix_identity::Identity;
use actix_multipart::form::{tempfile::TempFile, text::Text, MultipartForm};
use actix_web::rt::spawn;
use actix_web::rt::task::spawn_blocking;
use actix_web::rt::time::timeout;
@ -56,6 +57,7 @@ impl From<AcAndGraph> for Bson {
}
#[derive(Clone, Default, Deserialize, Serialize)]
#[serde(tag = "type", content = "content")]
pub(crate) enum OptionWithError<T> {
Some(T),
Error(String),
@ -182,11 +184,35 @@ pub(crate) struct AdfProblem {
pub(crate) acs_per_strategy: AcsPerStrategy,
}
#[derive(Clone, Deserialize)]
struct AddAdfProblemBody {
name: Option<String>,
#[derive(MultipartForm)]
struct AddAdfProblemBodyMultipart {
name: Text<String>,
code: Option<Text<String>>, // Either Code or File is set
file: Option<TempFile>, // Either Code or File is set
parsing: Text<Parsing>,
}
#[derive(Clone)]
struct AddAdfProblemBodyPlain {
name: String,
code: String,
parse_strategy: Parsing,
parsing: Parsing,
}
impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
type Error = &'static str;
fn try_from(source: AddAdfProblemBodyMultipart) -> Result<Self, Self::Error> {
Ok(Self {
name: source.name.into_inner(),
code: source
.file
.map(|f| std::io::read_to_string(f.file).expect("TempFile should be readable"))
.or_else(|| source.code.map(|c| c.into_inner()))
.ok_or("Either a file or the code has to be provided.")?,
parsing: source.parsing.into_inner(),
})
}
}
async fn adf_problem_exists(
@ -233,9 +259,12 @@ async fn add_adf_problem(
req: HttpRequest,
app_state: web::Data<AppState>,
identity: Option<Identity>,
req_body: web::Json<AddAdfProblemBody>,
req_body: MultipartForm<AddAdfProblemBodyMultipart>,
) -> impl Responder {
let adf_problem_input: AddAdfProblemBody = req_body.into_inner();
let adf_problem_input: AddAdfProblemBodyPlain = match req_body.into_inner().try_into() {
Ok(input) => input,
Err(err) => return HttpResponse::BadRequest().body(err),
};
let adf_coll: mongodb::Collection<AdfProblem> = app_state
.mongodb_client
.database(DB_NAME)
@ -291,35 +320,32 @@ async fn add_adf_problem(
Some(Ok(username)) => username,
};
let problem_name = match &adf_problem_input.name {
Some(name) => {
if adf_problem_exists(&adf_coll, name, &username).await {
return HttpResponse::Conflict()
.body("ADF Problem with that name already exists. Please pick another one!");
}
name.clone()
let problem_name = if !adf_problem_input.name.is_empty() {
if adf_problem_exists(&adf_coll, &adf_problem_input.name, &username).await {
return HttpResponse::Conflict()
.body("ADF Problem with that name already exists. Please pick another one!");
}
None => {
let gen = Generator::with_naming(Name::Numbered);
let candidates = gen.take(10);
let mut name: Option<String> = None;
for candidate in candidates {
if name.is_some() {
continue;
}
adf_problem_input.name.clone()
} else {
let gen = Generator::with_naming(Name::Numbered);
let candidates = gen.take(10);
if !(adf_problem_exists(&adf_coll, &candidate, &username).await) {
name = Some(candidate);
}
let mut name: Option<String> = None;
for candidate in candidates {
if name.is_some() {
continue;
}
match name {
Some(name) => name,
None => {
return HttpResponse::InternalServerError().body("Could not generate new name.")
}
if !(adf_problem_exists(&adf_coll, &candidate, &username).await) {
name = Some(candidate);
}
}
match name {
Some(name) => name,
None => {
return HttpResponse::InternalServerError().body("Could not generate new name.")
}
}
};
@ -328,7 +354,7 @@ async fn add_adf_problem(
name: problem_name.clone(),
username: username.clone(),
code: adf_problem_input.code.clone(),
parsing_used: adf_problem_input.parse_strategy,
parsing_used: adf_problem_input.parsing,
adf: SimplifiedAdfOpt::None,
acs_per_strategy: AcsPerStrategy::default(),
};
@ -365,7 +391,7 @@ async fn add_adf_problem(
parser.parse()(&adf_problem_input.code)
.map_err(|_| "ADF could not be parsed, double check your input!")?;
let lib_adf = match adf_problem_input.parse_strategy {
let lib_adf = match adf_problem_input.parsing {
Parsing::Naive => Adf::from_parser(&parser),
Parsing::Hybrid => {
let bd_adf = BdAdf::from_parser(&parser);

View File

@ -18,6 +18,7 @@ pub(crate) const USER_COLL: &str = "users";
pub(crate) const ADF_COLL: &str = "adf-problems";
#[derive(Copy, Clone, PartialEq, Eq, Hash, Serialize)]
#[serde(tag = "type", content = "content")]
pub(crate) enum Task {
Parse,
Solve(Strategy),

View File

@ -110,39 +110,44 @@ async fn delete_account(
.database(DB_NAME)
.collection(ADF_COLL);
match identity.map(|id| id.id()) {
None => HttpResponse::Unauthorized().body("You need to login to delete your account."),
Some(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
Some(Ok(username)) => {
// Delete all adfs created by user
match adf_coll
.delete_many(doc! { "username": &username }, None)
.await
{
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(DeleteResult {
deleted_count: _, ..
}) => {
// Delete actual user
match user_coll
.delete_one(doc! { "username": &username }, None)
.await
{
Ok(DeleteResult {
deleted_count: 0, ..
}) => HttpResponse::InternalServerError()
.body("Account could not be deleted."),
Ok(DeleteResult {
deleted_count: 1, ..
}) => HttpResponse::Ok().body("Account deleted."),
Ok(_) => unreachable!(
match identity {
None => HttpResponse::Unauthorized().body("You are not logged in."),
Some(id) => match id.id() {
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(username) => {
// Delete all adfs created by user
match adf_coll
.delete_many(doc! { "username": &username }, None)
.await
{
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(DeleteResult {
deleted_count: _, ..
}) => {
// Delete actual user
match user_coll
.delete_one(doc! { "username": &username }, None)
.await
{
Ok(DeleteResult {
deleted_count: 0, ..
}) => HttpResponse::InternalServerError()
.body("Account could not be deleted."),
Ok(DeleteResult {
deleted_count: 1, ..
}) => {
id.logout();
HttpResponse::Ok().body("Account deleted.")
}
Ok(_) => unreachable!(
"delete_one removes at most one entry so all cases are covered already"
),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
}
}
}
}
},
}
}
@ -237,28 +242,33 @@ async fn user_info(app_state: web::Data<AppState>, identity: Option<Identity>) -
.database(DB_NAME)
.collection(USER_COLL);
match identity.map(|id| id.id()) {
match identity {
None => {
HttpResponse::Unauthorized().body("You need to login get your account information.")
}
Some(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
Some(Ok(username)) => {
match user_coll
.find_one(doc! { "username": &username }, None)
.await
{
Ok(Some(user)) => {
let info = UserInfo {
username: user.username,
temp: user.password.is_none(),
};
Some(id) => match id.id() {
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(username) => {
match user_coll
.find_one(doc! { "username": &username }, None)
.await
{
Ok(Some(user)) => {
let info = UserInfo {
username: user.username,
temp: user.password.is_none(),
};
HttpResponse::Ok().json(info)
HttpResponse::Ok().json(info)
}
Ok(None) => {
id.logout();
HttpResponse::NotFound().body("Logged in user does not exist anymore.")
}
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
Ok(None) => HttpResponse::NotFound().body("Logged in user does not exist anymore."),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
}
},
}
}