mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
1 Commits
c8ab6db93d
...
7b6f98c934
| Author | SHA1 | Date | |
|---|---|---|---|
|
7b6f98c934 |
@ -1,5 +1,4 @@
|
||||
frontend/node_modules
|
||||
frontend/.parcel-cache
|
||||
server/mongodb-data
|
||||
target/debug
|
||||
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
# 1. BUILD-CONTAINER: Frontend
|
||||
FROM node:hydrogen-alpine
|
||||
FROM node:gallium-alpine
|
||||
|
||||
WORKDIR /root
|
||||
|
||||
@ -30,7 +30,5 @@ WORKDIR /root
|
||||
COPY --from=0 /root/dist /root/assets
|
||||
COPY --from=1 /root/target/release/adf-bdd-server /root/server
|
||||
|
||||
EXPOSE 8080
|
||||
|
||||
ENTRYPOINT ["./server"]
|
||||
|
||||
|
||||
@ -1,33 +1,14 @@
|
||||
import React, {
|
||||
useState, useContext, useEffect, useCallback, useRef,
|
||||
} from 'react';
|
||||
import { useParams, useNavigate } from 'react-router-dom';
|
||||
import {
|
||||
Alert,
|
||||
AlertColor,
|
||||
Button,
|
||||
Chip,
|
||||
Container,
|
||||
Paper,
|
||||
Pagination,
|
||||
Skeleton,
|
||||
Stack,
|
||||
Tabs,
|
||||
Tab,
|
||||
TextField,
|
||||
Typography,
|
||||
} from '@mui/material';
|
||||
import React from 'react';
|
||||
|
||||
import GraphG6, { GraphProps } from './graph-g6';
|
||||
import LoadingContext from './loading-context';
|
||||
import SnackbarContext from './snackbar-context';
|
||||
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 const STRATEGIES_WITHOUT_PARSE: StrategyCamelCase[] = ['Ground', 'Complete', 'Stable', 'StableCountingA', 'StableCountingB', 'StableNogood'];
|
||||
|
||||
export interface AcAndGraph {
|
||||
ac: string[],
|
||||
@ -55,8 +36,7 @@ export interface AdfProblemInfo {
|
||||
name: string,
|
||||
code: string,
|
||||
parsing_used: Parsing,
|
||||
// NOTE: the keys are really only strategies
|
||||
acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt },
|
||||
acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt }, // NOTE: the keys are really only strategies
|
||||
running_tasks: Task[],
|
||||
}
|
||||
|
||||
@ -66,11 +46,9 @@ export function acsWithGraphOptToColor(status: AcsWithGraphsOpt, running: boolea
|
||||
}
|
||||
|
||||
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)');
|
||||
case 'None': return 'info';
|
||||
case 'Error': return 'error';
|
||||
case 'Some': return 'success';
|
||||
}
|
||||
}
|
||||
|
||||
@ -80,261 +58,15 @@ export function acsWithGraphOptToText(status: AcsWithGraphsOpt, running: boolean
|
||||
}
|
||||
|
||||
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)');
|
||||
case 'None': return 'Not attempted';
|
||||
case 'Error': return 'Failed';
|
||||
case 'Some': return 'Done';
|
||||
}
|
||||
}
|
||||
|
||||
function AdfDetails() {
|
||||
const { adfName } = useParams();
|
||||
const navigate = useNavigate();
|
||||
|
||||
const { setLoading } = useContext(LoadingContext);
|
||||
const { status: snackbarInfo, setStatus: setSnackbarInfo } = useContext(SnackbarContext);
|
||||
const [problem, setProblem] = useState<AdfProblemInfo>();
|
||||
const [tab, setTab] = useState<StrategySnakeCase>('parse_only');
|
||||
const [solutionIndex, setSolutionIndex] = useState<number>(0);
|
||||
|
||||
const isFirstRender = useRef(true);
|
||||
|
||||
const fetchProblem = useCallback(
|
||||
() => {
|
||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/${adfName}`, {
|
||||
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((resProblem) => {
|
||||
setProblem(resProblem);
|
||||
});
|
||||
break;
|
||||
default:
|
||||
navigate('/');
|
||||
break;
|
||||
}
|
||||
});
|
||||
},
|
||||
[setProblem],
|
||||
);
|
||||
|
||||
const solveHandler = useCallback(
|
||||
(strategy: StrategyCamelCase) => {
|
||||
setLoading(true);
|
||||
|
||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/${adfName}/solve`, {
|
||||
method: 'PUT',
|
||||
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
|
||||
headers: {
|
||||
'Content-Type': 'application/json',
|
||||
},
|
||||
body: JSON.stringify({ strategy }),
|
||||
})
|
||||
.then((res) => {
|
||||
switch (res.status) {
|
||||
case 200:
|
||||
setSnackbarInfo({ message: 'Solving problem now...', severity: 'success', potentialUserChange: false });
|
||||
fetchProblem();
|
||||
break;
|
||||
default:
|
||||
setSnackbarInfo({ message: 'Something went wrong tying to solve the problem.', severity: 'error', potentialUserChange: false });
|
||||
break;
|
||||
}
|
||||
})
|
||||
.finally(() => setLoading(false));
|
||||
},
|
||||
[adfName],
|
||||
);
|
||||
|
||||
const deleteHandler = useCallback(
|
||||
() => {
|
||||
setLoading(true);
|
||||
|
||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/${adfName}`, {
|
||||
method: 'DELETE',
|
||||
credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
|
||||
headers: {
|
||||
'Content-Type': 'application/json',
|
||||
},
|
||||
})
|
||||
.then((res) => {
|
||||
switch (res.status) {
|
||||
case 200:
|
||||
setSnackbarInfo({ message: 'ADF Problem deleted.', severity: 'success', potentialUserChange: false });
|
||||
navigate('/');
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
})
|
||||
.finally(() => setLoading(false));
|
||||
},
|
||||
[adfName],
|
||||
);
|
||||
|
||||
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;
|
||||
|
||||
fetchProblem();
|
||||
}
|
||||
},
|
||||
[snackbarInfo?.potentialUserChange],
|
||||
);
|
||||
|
||||
useEffect(
|
||||
() => {
|
||||
// if there is a running task, fetch problems again after 20 seconds
|
||||
let timeout: ReturnType<typeof setTimeout>;
|
||||
if (problem && problem.running_tasks.length > 0) {
|
||||
timeout = setTimeout(() => fetchProblem(), 20000);
|
||||
}
|
||||
|
||||
return () => {
|
||||
if (timeout) {
|
||||
clearTimeout(timeout);
|
||||
}
|
||||
};
|
||||
},
|
||||
[problem],
|
||||
);
|
||||
|
||||
const acsOpt = problem?.acs_per_strategy[tab];
|
||||
const acsContent = acsOpt?.type === 'Some' ? acsOpt.content : undefined;
|
||||
const tabCamelCase: StrategyCamelCase = tab.replace(/^([a-z])/, (_, p1) => p1.toUpperCase()).replace(/_([a-z])/g, (_, p1) => `${p1.toUpperCase()}`) as StrategyCamelCase;
|
||||
|
||||
return (
|
||||
<>
|
||||
<Typography variant="h3" component="h1" align="center" gutterBottom>
|
||||
ADF-BDD.DEV
|
||||
</Typography>
|
||||
<Container sx={{ marginBottom: 4 }}>
|
||||
{problem ? (
|
||||
<>
|
||||
<Paper elevation={8} sx={{ padding: 2, marginBottom: 2 }}>
|
||||
<Stack direction="row" justifyContent="space-between" sx={{ marginBottom: 1 }}>
|
||||
<Button
|
||||
variant="outlined"
|
||||
color="info"
|
||||
onClick={() => { navigate('/'); }}
|
||||
>
|
||||
Back
|
||||
</Button>
|
||||
<Typography variant="h4" component="h2" align="center" gutterBottom>
|
||||
{problem.name}
|
||||
</Typography>
|
||||
<Button
|
||||
type="button"
|
||||
variant="outlined"
|
||||
color="error"
|
||||
onClick={() => {
|
||||
// eslint-disable-next-line no-alert
|
||||
if (window.confirm('Are you sure that you want to delete this ADF problem?')) {
|
||||
deleteHandler();
|
||||
}
|
||||
}}
|
||||
>
|
||||
Delete
|
||||
</Button>
|
||||
</Stack>
|
||||
<TextField
|
||||
name="code"
|
||||
label="Code"
|
||||
helperText="Click here to copy!"
|
||||
multiline
|
||||
maxRows={5}
|
||||
fullWidth
|
||||
variant="filled"
|
||||
value={problem.code.trim()}
|
||||
disabled
|
||||
sx={{ cursor: 'pointer' }}
|
||||
onClick={() => { navigator.clipboard.writeText(problem.code); setSnackbarInfo({ message: 'Code copied to clipboard!', severity: 'info', potentialUserChange: false }); }}
|
||||
/>
|
||||
</Paper>
|
||||
<Tabs
|
||||
value={tab}
|
||||
onChange={(_e, newTab) => { setTab(newTab); setSolutionIndex(0); }}
|
||||
variant="scrollable"
|
||||
scrollButtons="auto"
|
||||
>
|
||||
<Tab wrapped value="parse_only" label={<Chip color={acsWithGraphOptToColor(problem.acs_per_strategy.parse_only, problem.running_tasks.some((t: Task) => t.type === 'Parse'))} label={`${problem.parsing_used} Parsing`} sx={{ cursor: 'inherit' }} />} />
|
||||
{STRATEGIES_WITHOUT_PARSE.map((strategy) => {
|
||||
const spaced = strategy.replace(/([A-Za-z])([A-Z])/g, '$1 $2');
|
||||
const snakeCase = strategy.replace(/^([A-Z])/, (_, p1) => p1.toLowerCase()).replace(/([A-Z])/g, (_, p1) => `_${p1.toLowerCase()}`) as StrategySnakeCase;
|
||||
const status = problem.acs_per_strategy[snakeCase];
|
||||
|
||||
const running = problem.running_tasks.some((t: Task) => t.type === 'Solve' && t.content === strategy);
|
||||
|
||||
const color = acsWithGraphOptToColor(status, running);
|
||||
|
||||
return <Tab key={strategy} wrapped value={snakeCase} label={<Chip color={color} label={spaced} sx={{ cursor: 'inherit' }} />} />;
|
||||
})}
|
||||
</Tabs>
|
||||
|
||||
{acsContent && acsContent.length > 1 && (
|
||||
<>
|
||||
Models:
|
||||
<br />
|
||||
<Pagination variant="outlined" shape="rounded" count={acsContent.length} page={solutionIndex + 1} onChange={(_e, newIdx) => setSolutionIndex(newIdx - 1)} />
|
||||
</>
|
||||
)}
|
||||
<Paper elevation={3} square sx={{ padding: 2, marginTop: 4, marginBottom: 4 }}>
|
||||
{problem.running_tasks.some((t: Task) => (tab === 'parse_only' && t.type === 'Parse') || (t.type === 'Solve' && t.content === tabCamelCase)) ? (
|
||||
<Alert severity="warning">Working hard to solve the problem right now...</Alert>
|
||||
) : (
|
||||
<>
|
||||
{acsContent && acsContent.length > 0 && (
|
||||
<GraphG6 graph={acsContent[solutionIndex].graph} />
|
||||
)}
|
||||
{acsContent && acsContent.length === 0 && (
|
||||
<Alert severity="info">The problem has no models for this strategy.</Alert>
|
||||
)}
|
||||
{!acsContent && acsOpt?.type === 'Error' && (
|
||||
<Alert severity="error">
|
||||
An error occurred:
|
||||
{acsOpt.content}
|
||||
</Alert>
|
||||
)}
|
||||
{!acsContent && acsOpt?.type === 'None' && (
|
||||
<>
|
||||
<Alert severity="info" sx={{ marginBottom: 1 }}>This strategy was not attempted yet.</Alert>
|
||||
<Button
|
||||
variant="contained"
|
||||
size="large"
|
||||
color="warning"
|
||||
onClick={() => {
|
||||
solveHandler(tabCamelCase);
|
||||
}}
|
||||
>
|
||||
Solve now!
|
||||
</Button>
|
||||
</>
|
||||
)}
|
||||
</>
|
||||
)}
|
||||
</Paper>
|
||||
</>
|
||||
) : (
|
||||
<>
|
||||
<Paper elevation={8} sx={{ padding: 2, marginBottom: 8 }}>
|
||||
<Skeleton variant="text" width="50%" sx={{ fontSize: '2.125rem', margin: 'auto' }} />
|
||||
<Skeleton variant="rounded" width="100%" height={200} />
|
||||
</Paper>
|
||||
<Skeleton variant="rectangular" width="100%" height={500} />
|
||||
</>
|
||||
)}
|
||||
</Container>
|
||||
</>
|
||||
<div>Details</div>
|
||||
);
|
||||
}
|
||||
|
||||
|
||||
@ -3,12 +3,16 @@ import React, {
|
||||
} from 'react';
|
||||
|
||||
import {
|
||||
Backdrop,
|
||||
Button,
|
||||
CircularProgress,
|
||||
CssBaseline,
|
||||
Container,
|
||||
FormControl,
|
||||
FormControlLabel,
|
||||
FormLabel,
|
||||
Link,
|
||||
Pagination,
|
||||
Paper,
|
||||
Radio,
|
||||
RadioGroup,
|
||||
@ -33,7 +37,7 @@ ac(b,b).
|
||||
ac(c,and(a,b)).
|
||||
ac(d,neg(b)).`;
|
||||
|
||||
function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
||||
function AdfNewForm({fetchProblems}: { fetchProblems: () => void; }) {
|
||||
const { setLoading } = useContext(LoadingContext);
|
||||
const { setStatus: setSnackbarInfo } = useContext(SnackbarContext);
|
||||
const [isFileUpload, setFileUpload] = useState(false);
|
||||
@ -50,10 +54,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
||||
const formData = new FormData();
|
||||
|
||||
if (isFileUpload && fileRef.current) {
|
||||
const file = fileRef.current.files?.[0];
|
||||
if (file) {
|
||||
formData.append('file', file);
|
||||
}
|
||||
formData.append('file', fileRef.current.files![0]);
|
||||
} else {
|
||||
formData.append('code', code);
|
||||
}
|
||||
@ -84,84 +85,84 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
||||
|
||||
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>
|
||||
<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>
|
||||
.
|
||||
</>
|
||||
{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); }}
|
||||
/>
|
||||
)}
|
||||
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>
|
||||
<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>
|
||||
);
|
||||
}
|
||||
|
||||
|
||||
@ -1,15 +1,21 @@
|
||||
import React, {
|
||||
useRef, useState, useCallback, useEffect, useContext,
|
||||
} from 'react';
|
||||
|
||||
import {
|
||||
useNavigate,
|
||||
} from 'react-router-dom';
|
||||
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,
|
||||
@ -17,29 +23,18 @@ import {
|
||||
TableCell,
|
||||
TableBody,
|
||||
Typography,
|
||||
TextField,
|
||||
ToggleButtonGroup,
|
||||
ToggleButton,
|
||||
} from '@mui/material';
|
||||
|
||||
import AdfNewForm from './adf-new-form';
|
||||
|
||||
import {
|
||||
AdfProblemInfo,
|
||||
StrategySnakeCase,
|
||||
STRATEGIES_WITHOUT_PARSE,
|
||||
Task,
|
||||
acsWithGraphOptToColor,
|
||||
acsWithGraphOptToText,
|
||||
} from './adf-details';
|
||||
|
||||
import SnackbarContext from './snackbar-context';
|
||||
import {AdfProblemInfo, StrategySnakeCase, StrategyCamelCase, Task, acsWithGraphOptToColor, acsWithGraphOptToText} from './adf-details';
|
||||
|
||||
function AdfOverview() {
|
||||
const { status: snackbarInfo } = useContext(SnackbarContext);
|
||||
const [problems, setProblems] = useState<AdfProblemInfo[]>([]);
|
||||
|
||||
const navigate = useNavigate();
|
||||
|
||||
const isFirstRender = useRef(true);
|
||||
|
||||
const fetchProblems = useCallback(
|
||||
() => {
|
||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/`, {
|
||||
@ -52,13 +47,10 @@ function AdfOverview() {
|
||||
.then((res) => {
|
||||
switch (res.status) {
|
||||
case 200:
|
||||
res.json().then((resProblems) => {
|
||||
setProblems(resProblems);
|
||||
res.json().then((problems) => {
|
||||
setProblems(problems);
|
||||
});
|
||||
break;
|
||||
case 401:
|
||||
setProblems([]);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
@ -68,72 +60,47 @@ function AdfOverview() {
|
||||
);
|
||||
|
||||
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],
|
||||
() => { fetchProblems(); },
|
||||
[],
|
||||
);
|
||||
|
||||
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],
|
||||
);
|
||||
// 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
|
||||
&& (
|
||||
{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}
|
||||
onClick={() => { navigate(`/${problem.name}`); }}
|
||||
sx={{ '&:last-child td, &:last-child th': { border: 0 }, cursor: 'pointer' }}
|
||||
>
|
||||
<TableCell component="th" scope="row">
|
||||
{problem.name}
|
||||
</TableCell>
|
||||
{
|
||||
<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');
|
||||
@ -141,30 +108,30 @@ function AdfOverview() {
|
||||
const color = acsWithGraphOptToColor(status, running);
|
||||
const text = acsWithGraphOptToText(status, running);
|
||||
|
||||
return <TableCell align="center"><Chip color={color} label={`${text} (${problem.parsing_used} Parsing)`} sx={{ cursor: 'inherit' }} /></TableCell>;
|
||||
return <TableCell align="center"><Chip color={color} label={`${text} (${problem.parsing_used} Parsing)`} /></TableCell>;
|
||||
})()
|
||||
}
|
||||
{
|
||||
STRATEGIES_WITHOUT_PARSE.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);
|
||||
{
|
||||
(['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);
|
||||
const color = acsWithGraphOptToColor(status, running);
|
||||
const text = acsWithGraphOptToText(status, running);
|
||||
|
||||
return <TableCell key={strategy} align="center"><Chip color={color} label={text} sx={{ cursor: 'inherit' }} /></TableCell>;
|
||||
})
|
||||
return <TableCell align="center"><Chip color={color} label={text} /></TableCell>;
|
||||
})
|
||||
}
|
||||
</TableRow>
|
||||
))}
|
||||
</TableBody>
|
||||
</Table>
|
||||
</TableContainer>
|
||||
</Paper>
|
||||
</Container>
|
||||
)}
|
||||
<AdfNewForm fetchProblems={fetchProblems} />
|
||||
</>
|
||||
</TableRow>
|
||||
))}
|
||||
</TableBody>
|
||||
</Table>
|
||||
</TableContainer>
|
||||
</Paper>
|
||||
</Container>
|
||||
}
|
||||
<AdfNewForm fetchProblems={fetchProblems} />
|
||||
</>
|
||||
);
|
||||
}
|
||||
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
import React, { useState, useMemo } from 'react';
|
||||
import * as React from 'react';
|
||||
|
||||
import { createBrowserRouter, RouterProvider } from 'react-router-dom';
|
||||
|
||||
@ -7,18 +7,33 @@ import {
|
||||
Alert,
|
||||
AlertColor,
|
||||
Backdrop,
|
||||
Button,
|
||||
CircularProgress,
|
||||
CssBaseline,
|
||||
Container,
|
||||
FormControl,
|
||||
FormControlLabel,
|
||||
FormLabel,
|
||||
Link,
|
||||
Pagination,
|
||||
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 browserRouter = createBrowserRouter([
|
||||
{
|
||||
path: '/',
|
||||
@ -34,11 +49,12 @@ function App() {
|
||||
const prefersDarkMode = useMediaQuery('(prefers-color-scheme: dark)');
|
||||
|
||||
const theme = useMemo(
|
||||
() => createTheme({
|
||||
palette: {
|
||||
mode: prefersDarkMode ? 'dark' : 'light',
|
||||
},
|
||||
}),
|
||||
() =>
|
||||
createTheme({
|
||||
palette: {
|
||||
mode: prefersDarkMode ? 'dark' : 'light',
|
||||
},
|
||||
}),
|
||||
[prefersDarkMode],
|
||||
);
|
||||
|
||||
@ -50,17 +66,14 @@ function App() {
|
||||
severity: AlertColor,
|
||||
potentialUserChange: boolean,
|
||||
} | undefined>();
|
||||
const snackbarContext = useMemo(
|
||||
() => ({ status: snackbarInfo, setStatus: setSnackbarInfo }),
|
||||
[snackbarInfo, setSnackbarInfo],
|
||||
);
|
||||
const snackbarContext = useMemo(() => ({ status: snackbarInfo, setStatus: setSnackbarInfo }), [snackbarInfo, setSnackbarInfo]);
|
||||
|
||||
return (
|
||||
<ThemeProvider theme={theme}>
|
||||
<LoadingContext.Provider value={loadingContext}>
|
||||
<SnackbarContext.Provider value={snackbarContext}>
|
||||
<CssBaseline />
|
||||
<main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
|
||||
<main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
|
||||
<RouterProvider router={browserRouter} />
|
||||
</main>
|
||||
<Footer />
|
||||
@ -83,4 +96,113 @@ function App() {
|
||||
);
|
||||
}
|
||||
|
||||
// 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;
|
||||
|
||||
@ -11,6 +11,7 @@ import {
|
||||
DialogActions,
|
||||
DialogContent,
|
||||
DialogTitle,
|
||||
Snackbar,
|
||||
TextField,
|
||||
Toolbar,
|
||||
} from '@mui/material';
|
||||
@ -77,7 +78,7 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
|
||||
.then((res) => {
|
||||
switch (res.status) {
|
||||
case 200:
|
||||
close(`Action '${del ? 'Delete' : formType}' successful!`, 'success');
|
||||
close(`Action '${formType}' successful!`, 'success');
|
||||
break;
|
||||
default:
|
||||
setError(true);
|
||||
@ -113,14 +114,13 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
|
||||
</DialogContent>
|
||||
<DialogActions>
|
||||
<Button type="button" onClick={() => close()}>Cancel</Button>
|
||||
<Button type="submit" variant="contained" color="success">{formType}</Button>
|
||||
<Button type="submit">{formType}</Button>
|
||||
{formType === UserFormType.Update
|
||||
// TODO: add another confirm dialog here
|
||||
&& (
|
||||
<Button
|
||||
type="button"
|
||||
variant="outlined"
|
||||
color="error"
|
||||
onClick={() => {
|
||||
// eslint-disable-next-line no-alert
|
||||
if (window.confirm('Are you sure that you want to delete your account?')) {
|
||||
@ -157,7 +157,7 @@ function Footer() {
|
||||
.then((res) => {
|
||||
switch (res.status) {
|
||||
case 200:
|
||||
setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: true });
|
||||
setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: false });
|
||||
setUsername(undefined);
|
||||
break;
|
||||
default:
|
||||
@ -168,8 +168,7 @@ function Footer() {
|
||||
}, [setSnackbarInfo]);
|
||||
|
||||
useEffect(() => {
|
||||
// TODO: having the info if the user may have changed on the snackbar info
|
||||
// is a bit lazy and unclean; be better!
|
||||
// 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;
|
||||
|
||||
@ -225,9 +224,7 @@ function Footer() {
|
||||
formType={dialogTypeOpen}
|
||||
close={(message, severity) => {
|
||||
setDialogTypeOpen(null);
|
||||
setSnackbarInfo((!!message && !!severity)
|
||||
? { message, severity, potentialUserChange: true }
|
||||
: undefined);
|
||||
setSnackbarInfo((!!message && !!severity) ? { message, severity, potentialUserChange: true } : undefined);
|
||||
}}
|
||||
username={dialogTypeOpen === UserFormType.Update ? username : undefined}
|
||||
/>
|
||||
|
||||
@ -183,7 +183,7 @@ function GraphG6(props: Props) {
|
||||
graphRef.current = new Graph({
|
||||
container: ref.current!,
|
||||
width: 1200,
|
||||
height: 400,
|
||||
height: 600,
|
||||
fitView: true,
|
||||
modes: {
|
||||
default: ['drag-canvas', 'zoom-canvas', 'drag-node'],
|
||||
@ -368,9 +368,7 @@ function GraphG6(props: Props) {
|
||||
<div style={{ padding: 4 }}>
|
||||
<span style={{ color: '#ed6c02', marginRight: 8 }}>lo edge (condition is false)</span>
|
||||
{' '}
|
||||
<span style={{ color: '#1976d2', marginRight: 8 }}>hi edge (condition is true)</span>
|
||||
{' '}
|
||||
Click nodes to hightlight paths! (You can also drag and zoom.)
|
||||
<span style={{ color: '#1976d2' }}>hi edge (condition is true)</span>
|
||||
</div>
|
||||
</>
|
||||
);
|
||||
|
||||
@ -1,24 +0,0 @@
|
||||
version: '3.1'
|
||||
|
||||
services:
|
||||
|
||||
mongo:
|
||||
image: mongo
|
||||
restart: always
|
||||
ports:
|
||||
- 27017:27017
|
||||
environment:
|
||||
MONGO_INITDB_ROOT_USERNAME: root
|
||||
MONGO_INITDB_ROOT_PASSWORD: example
|
||||
volumes:
|
||||
- ./mongodb-data:/data/db
|
||||
|
||||
mongo-express:
|
||||
image: mongo-express
|
||||
restart: always
|
||||
ports:
|
||||
- 8081:8081
|
||||
environment:
|
||||
ME_CONFIG_MONGODB_ADMINUSERNAME: root
|
||||
ME_CONFIG_MONGODB_ADMINPASSWORD: example
|
||||
ME_CONFIG_MONGODB_URL: mongodb://root:example@mongo:27017/
|
||||
@ -28,13 +28,13 @@ use crate::user::{username_exists, User};
|
||||
type Ac = Vec<Term>;
|
||||
type AcDb = Vec<String>;
|
||||
|
||||
#[derive(Copy, Clone, Debug, Deserialize, Serialize)]
|
||||
#[derive(Copy, Clone, Deserialize, Serialize)]
|
||||
pub(crate) enum Parsing {
|
||||
Naive,
|
||||
Hybrid,
|
||||
}
|
||||
|
||||
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize, Serialize)]
|
||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Deserialize, Serialize)]
|
||||
pub(crate) enum Strategy {
|
||||
Ground,
|
||||
Complete,
|
||||
@ -209,7 +209,6 @@ impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
|
||||
.file
|
||||
.map(|f| std::io::read_to_string(f.file).expect("TempFile should be readable"))
|
||||
.or_else(|| source.code.map(|c| c.into_inner()))
|
||||
.and_then(|code| (!code.is_empty()).then_some(code))
|
||||
.ok_or("Either a file or the code has to be provided.")?,
|
||||
parsing: source.parsing.into_inner(),
|
||||
})
|
||||
@ -389,25 +388,21 @@ async fn add_adf_problem(
|
||||
std::thread::sleep(Duration::from_secs(20));
|
||||
|
||||
let parser = AdfParser::default();
|
||||
let parse_result = parser.parse()(&adf_problem_input.code)
|
||||
.map_err(|_| "ADF could not be parsed, double check your input!");
|
||||
parser.parse()(&adf_problem_input.code)
|
||||
.map_err(|_| "ADF could not be parsed, double check your input!")?;
|
||||
|
||||
let result = parse_result.map(|_| {
|
||||
let lib_adf = match adf_problem_input.parsing {
|
||||
Parsing::Naive => Adf::from_parser(&parser),
|
||||
Parsing::Hybrid => {
|
||||
let bd_adf = BdAdf::from_parser(&parser);
|
||||
bd_adf.hybrid_step_opt(false)
|
||||
}
|
||||
};
|
||||
let lib_adf = match adf_problem_input.parsing {
|
||||
Parsing::Naive => Adf::from_parser(&parser),
|
||||
Parsing::Hybrid => {
|
||||
let bd_adf = BdAdf::from_parser(&parser);
|
||||
bd_adf.hybrid_step_opt(false)
|
||||
}
|
||||
};
|
||||
|
||||
let ac_and_graph = AcAndGraph {
|
||||
ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(),
|
||||
graph: lib_adf.into_double_labeled_graph(None),
|
||||
};
|
||||
|
||||
(SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph)
|
||||
});
|
||||
let ac_and_graph = AcAndGraph {
|
||||
ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(),
|
||||
graph: lib_adf.into_double_labeled_graph(None),
|
||||
};
|
||||
|
||||
app_state
|
||||
.currently_running
|
||||
@ -415,7 +410,7 @@ async fn add_adf_problem(
|
||||
.unwrap()
|
||||
.remove(&running_info);
|
||||
|
||||
result
|
||||
Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph))
|
||||
}),
|
||||
);
|
||||
|
||||
@ -515,30 +510,24 @@ async fn solve_adf_problem(
|
||||
Strategy::StableNogood => adf_problem.acs_per_strategy.stable_nogood.is_some(),
|
||||
};
|
||||
|
||||
let username_clone = username.clone();
|
||||
let problem_name_clone = problem_name.clone();
|
||||
|
||||
let running_info = RunningInfo {
|
||||
username: username_clone,
|
||||
adf_name: problem_name_clone,
|
||||
task: Task::Solve(adf_problem_input.strategy),
|
||||
};
|
||||
|
||||
// NOTE: we could also return the result here instead of throwing an error but I think the canonical way should just be to call the get endpoint for the problem.
|
||||
if has_been_solved
|
||||
|| app_state
|
||||
.currently_running
|
||||
.lock()
|
||||
.unwrap()
|
||||
.contains(&running_info)
|
||||
{
|
||||
if has_been_solved {
|
||||
return HttpResponse::Conflict()
|
||||
.body("The ADF problem has already been solved with this strategy. You can just get the solution from the problem data directly.");
|
||||
}
|
||||
|
||||
let username_clone = username.clone();
|
||||
let problem_name_clone = problem_name.clone();
|
||||
|
||||
let acs_and_graphs_fut = timeout(
|
||||
COMPUTE_TIME,
|
||||
spawn_blocking(move || {
|
||||
let running_info = RunningInfo {
|
||||
username: username_clone,
|
||||
adf_name: problem_name_clone,
|
||||
task: Task::Solve(adf_problem_input.strategy),
|
||||
};
|
||||
|
||||
app_state
|
||||
.currently_running
|
||||
.lock()
|
||||
|
||||
@ -17,14 +17,14 @@ pub(crate) const DB_NAME: &str = "adf-obdd";
|
||||
pub(crate) const USER_COLL: &str = "users";
|
||||
pub(crate) const ADF_COLL: &str = "adf-problems";
|
||||
|
||||
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Serialize)]
|
||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Serialize)]
|
||||
#[serde(tag = "type", content = "content")]
|
||||
pub(crate) enum Task {
|
||||
Parse,
|
||||
Solve(Strategy),
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
#[derive(Clone, PartialEq, Eq, Hash)]
|
||||
pub(crate) struct RunningInfo {
|
||||
pub(crate) username: String,
|
||||
pub(crate) adf_name: String,
|
||||
|
||||
@ -43,12 +43,6 @@ async fn main() -> std::io::Result<()> {
|
||||
// cookie secret ket
|
||||
let secret_key = Key::generate();
|
||||
|
||||
// needs to be set outside of httpserver closure to only create it once!
|
||||
let app_data = web::Data::new(AppState {
|
||||
mongodb_client: client.clone(),
|
||||
currently_running: Mutex::new(HashSet::new()),
|
||||
});
|
||||
|
||||
HttpServer::new(move || {
|
||||
let app = App::new();
|
||||
|
||||
@ -68,34 +62,37 @@ async fn main() -> std::io::Result<()> {
|
||||
#[cfg(not(feature = "cors_for_local_development"))]
|
||||
let cookie_secure = true;
|
||||
|
||||
app.app_data(app_data.clone())
|
||||
.wrap(IdentityMiddleware::default())
|
||||
.wrap(
|
||||
SessionMiddleware::builder(CookieSessionStore::default(), secret_key.clone())
|
||||
.cookie_name("adf-obdd-service-auth".to_owned())
|
||||
.cookie_secure(cookie_secure)
|
||||
.session_lifecycle(PersistentSession::default().session_ttl(COOKIE_DURATION))
|
||||
.build(),
|
||||
)
|
||||
.service(
|
||||
web::scope("/users")
|
||||
.service(register)
|
||||
.service(delete_account)
|
||||
.service(login)
|
||||
.service(logout)
|
||||
.service(user_info)
|
||||
.service(update_user),
|
||||
)
|
||||
.service(
|
||||
web::scope("/adf")
|
||||
.service(add_adf_problem)
|
||||
.service(solve_adf_problem)
|
||||
.service(get_adf_problem)
|
||||
.service(delete_adf_problem)
|
||||
.service(get_adf_problems_for_user),
|
||||
)
|
||||
// this mus be last to not override anything
|
||||
.service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
|
||||
app.app_data(web::Data::new(AppState {
|
||||
mongodb_client: client.clone(),
|
||||
currently_running: Mutex::new(HashSet::new()),
|
||||
}))
|
||||
.wrap(IdentityMiddleware::default())
|
||||
.wrap(
|
||||
SessionMiddleware::builder(CookieSessionStore::default(), secret_key.clone())
|
||||
.cookie_name("adf-obdd-service-auth".to_owned())
|
||||
.cookie_secure(cookie_secure)
|
||||
.session_lifecycle(PersistentSession::default().session_ttl(COOKIE_DURATION))
|
||||
.build(),
|
||||
)
|
||||
.service(
|
||||
web::scope("/users")
|
||||
.service(register)
|
||||
.service(delete_account)
|
||||
.service(login)
|
||||
.service(logout)
|
||||
.service(user_info)
|
||||
.service(update_user),
|
||||
)
|
||||
.service(
|
||||
web::scope("/adf")
|
||||
.service(add_adf_problem)
|
||||
.service(solve_adf_problem)
|
||||
.service(get_adf_problem)
|
||||
.service(delete_adf_problem)
|
||||
.service(get_adf_problems_for_user),
|
||||
)
|
||||
// this mus be last to not override anything
|
||||
.service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
|
||||
})
|
||||
.bind(("0.0.0.0", 8080))?
|
||||
.run()
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user