Commit eee43ce8 authored by Felix Freiberger's avatar Felix Freiberger
Browse files

Merge branch 'edge' into impress-cpw

parents db440f97 8e25ab75
......@@ -457,6 +457,13 @@ To use a worker, developers can use the API given by the factory \js{taskManager
This method will not forcefully terminate a worker that got stuck, and there is no method that will. Always ensure that all task functions in your worker terminate regularly.
\end{remark}
\item
\js{isTerminating()} returns whether the termination of the worker has been started.
\begin{remark}
It is not possible to decide whether the worker is terminating or has terminated already. In both cases, \js{isTerminating()} will return \js{true}.
\end{remark}
\item
\js{submitTask(taskName, data, resultCallback, cancellationCallback, priority)} submits a task to the worker to be executed. This function must not be called if the worker is terminating or has terminated.
......@@ -1284,6 +1291,15 @@ Correctness of this approach follows from the correctness of the corresponding a
\paragraph{To ensure the result is observation congruent} (in addition to being weakly bisimilar), a $\tau$ self loop is added to the new initial state if and only if the initial system contained a strong $\tau$-transition from its initial state to another state \emph{which ends up in the partition that contains the initial state}.
\section{Events and Layouting}
Most of \pcdc{} is layouted automatically by the browser, because most of the layout is defined in CSS. However, a few components use JavaScript to determine there size, for example the text editor or the file edit page (which tries to use exactly the available height).
These components need to be informed when they need to re-compute their layout. Additionally, a single step of re-layouting may not suffice, since a change might lead to further changes, for example by hiding a scrollbar.
This is implemented by two events: When a component detects or causes a change in the page geometry (for example because the user resized the window), a \js{contentSizeChanged} event is issue. This is caught in the root scope, where multiple \js{updateSizes} events are issued in successive digest cycles. All components are expected to adapt to a change in their size when they encounter this event.
\section{The Server Component of \pcdc{}}\label{sect:pseucoserver}
\Pcdc{} mostly is a JavaScript-application, running client-side in the browser. This only requires a HTTP server to deliver the (static) application files. However, there are two features that use an active server component:
......
......@@ -183,10 +183,12 @@
return;
}
if (!data.sharingAgreementVersion || data.sharingAgreementVersion < minSharingAgreementVersion) {
log(ip, "sent sharingAgreementVersion " + data.sharingAgreementVersion + ", which is too low");
errorResponse(res, "please update your client");
return;
if (!data.temporary) {
if (!data.sharingAgreementVersion || data.sharingAgreementVersion < minSharingAgreementVersion) {
log(ip, "sent sharingAgreementVersion " + data.sharingAgreementVersion + ", which is too low");
errorResponse(res, "please update your client");
return;
}
}
var id = generateRandomId();
......
......@@ -24,7 +24,7 @@
.trace .trace-state {
word-wrap: break-word;
font-family: Menlo,Monace,Consolas,"Courier New",monospace;
font-weight: 500;
color: #666666;
white-space: pre-wrap;
}
......@@ -32,7 +32,7 @@
word-wrap: break-word;
font-family: Menlo,Monace,Consolas,"Courier New",monospace;
padding-left: 0px;
color: #666666;
font-weight: 500;
white-space: pre-wrap;
}
......
......@@ -182,6 +182,9 @@ angular.module('cp.actions', [])
scope.working = true;
scope.cancellationPending = false;
scope.exportedData = null;
scope.error = null;
scope.task = worker.submitTask('exportLts', {
exportFormat: exportFormat,
dataId: dataId
......
......@@ -103,6 +103,9 @@ angular.module('cp.ui').directive('editorManager', function ($compile, _, $, Ham
};
applyPositions();
function broadcastIfDefined (scope, event) {
if (scope) scope.$broadcast(event);
}
// set up events
function tryPushSeparator (separator, diff, secondTry) {
......@@ -143,17 +146,18 @@ angular.module('cp.ui').directive('editorManager', function ($compile, _, $, Ham
if (window.element.width() < minWindowSizeBeforeMinimized) {
if (!window.minimized) {
window.element.addClass('minimized');
window.element.find('.ng-isolate-scope').isolateScope().$broadcast('minimized');
broadcastIfDefined(window.element.find('.ng-isolate-scope').isolateScope(), 'minimized');
window.minimized = true;
}
} else {
if (window.minimized) {
window.element.removeClass('minimized');
window.element.find('.ng-isolate-scope').isolateScope().$broadcast('restored');
broadcastIfDefined(window.element.find('.ng-isolate-scope').isolateScope(), 'restored');
window.minimized = false;
}
}
};
updateMinifiedStateForWindow(separator.leftWindow);
updateMinifiedStateForWindow(separator.rightWindow);
}
......@@ -184,7 +188,7 @@ angular.module('cp.ui').directive('editorManager', function ($compile, _, $, Ham
if (lastEvent) {
var diff = event.deltaX - lastEvent.deltaX;
tryPushSeparator(separator, diff);
scope.$broadcast('updateSizes');
scope.$emit('contentSizeChanged');
}
if (event.type === 'panend') {
......@@ -199,7 +203,7 @@ angular.module('cp.ui').directive('editorManager', function ($compile, _, $, Ham
var window = windows[i];
if (window.leftSeparator) tryPushSeparator(window.leftSeparator, -Infinity);
if (window.rightSeparator) tryPushSeparator(window.rightSeparator, Infinity);
scope.$broadcast('updateSizes');
scope.$emit('contentSizeChanged');
};
scope.fork = function (i) {
......
......@@ -13,27 +13,38 @@ var workerData;
};
var getCleanedLtsCopy = function (lts) {
var getCleanedLtsCopy = function (lts, failOnError) {
var ltsCopy = {
initialState: lts.initialState,
states: _.object(_.keys(lts.states), _.map(lts.states, function (state) {
return {
transitions: state.transitions ? _.map(state.transitions, function (transition) {
if (transition.weak) {
return {
weak: true,
detailsLabel: transition.detailsLabel,
target: transition.target,
};
} else {
return {
label: transition.label,
detailsLabel: transition.detailsLabel,
target: transition.target,
};
}
}) : null
};
if (state.transitions) {
return {
transitions: _.map(state.transitions, function (transition) {
if (transition.weak) {
return {
weak: true,
detailsLabel: transition.detailsLabel,
target: transition.target,
};
} else {
return {
label: transition.label,
detailsLabel: transition.detailsLabel,
target: transition.target,
};
}
})
};
} else {
if (failOnError) {
throw {
name: "LtsException",
message: "The outgoing transitions for one of the states are unknown.",
};
} else {
return { transient: null };
}
}
}))
};
......@@ -43,7 +54,7 @@ var workerData;
var exportLtsAsJson = function (lts, pretty) {
// only export whitelistes attributes
var ltsCopy = getCleanedLtsCopy(lts);
var ltsCopy = getCleanedLtsCopy(lts, true);
return pretty ? JSON.stringify(ltsCopy, null, 4) : JSON.stringify(ltsCopy);
};
......@@ -68,6 +79,13 @@ var workerData;
var startIndex = getIndex(stateName) + 1;
var state = lts.states[stateName];
if (!state.transitions) {
throw {
name: "LtsException",
message: "The outgoing transitions for one of the states are unknown.",
};
}
_.map(state.transitions, function (transition) {
transitionCount++;
......@@ -98,8 +116,14 @@ var workerData;
var getTransitionLabel = function (transition) {
if (transition.weak) return "i";
if (transition.label === 'i') throw "AUT cannot express strong \"i\" transitions.";
if (!/^[\x20-\x7E]*$/.test(transition.label)) throw "AUT cannot express this transition label: " + transition.label;
if (transition.label === 'i') throw {
name: "AutFormatException",
message: "AUT cannot express strong \"i\" transitions."
};
if (!/^[\x20-\x7E]*$/.test(transition.label)) throw {
name: "AutFormatException",
message: "AUT cannot express this transition label: " + transition.label
};
if (/^[a-zA-Z][a-zA-Z0-9_]*$/.test(transition.label)) return transition.label; // no double quotes needed
return '"' + transition.label + '"';
};
......@@ -109,6 +133,13 @@ var workerData;
var state = lts.states[stateName];
if (!state.transitions) {
throw {
name: "LtsException",
message: "The outgoing transitions for one of the states are unknown.",
};
}
_.map(state.transitions, function (transition) {
transitionCount++;
......@@ -130,6 +161,13 @@ var workerData;
_.map(states, function (stateName) {
var state = lts.states[stateName];
if (!state.transitions) {
throw {
name: "LtsException",
message: "The outgoing transitions for one of the states are unknown.",
};
}
_.map(state.transitions, function (transition) {
transitions += ' "' + stateName + '" -> "' + transition.target + '" [label="' + getExportableLabel(transition) + '"];\n';
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment