goals.tex revision bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
d29201dd5328b88140ce050100693c501852657dChristian Maeder% Ligatur-Problem (z.b. bei specific wird aus dem fi eine ligatur
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder% gemacht, danach nicht mehr suchbar im acrobat-reader) wird mit
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder% diesem Eintrag behoben. Toll!
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc%%%%%%%%%%%%%%%%%%%%%%%%%%
cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen Kuksa\RequirePackage{ifpdf}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\RequirePackage{cmap}% Improve PDF text search.
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\documentclass[11pt,draft,a4paper]{article}%{scrartcl}%{report}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\usepackage{xspace}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\usepackage{amsmath}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\newcommand{\freecad}{FreeCAD\xspace}
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder\newcommand{\opencasc}{Open CASCADE\xspace}
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\newcommand{\hets}{Hets\xspace}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\newcommand{\bash}[1]{{\tt #1}}
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc\newcommand{\haskell}[1]{{\tt #1}}
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc\newcommand{\setsep}[2]{\{#1~|~#2\}}
6342ef8f9f785e79c91f217c30b3ba2b6fa0ad4fEugen Kuksa\newcommand{\leftsem}{[\![} %%
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\newcommand{\rightsem}{]\!]} %%
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc\newcommand{\setsem}[1]{\leftsem #1 \rightsem} %% set semantics
d386b61802c70e3d220d4520d9fcdefbd9c469f4Soeren D. Schulze\begin{document}
0ac66bed6456d7900a657269e36107ca7bec4756Iulia Ignatov\title{Internship Goals for Robert Savu}
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa\author{Ewaryst Schulz}
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder\section{Reading \freecad documents}
e16b3696b2c173aac14200321868ed81b8f7dc69Christian MaederGiven a document containing a \freecad design (typically a *.fcstd-file) we want to import it into \hets. This requires the following:
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder\begin{description}
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder \item[Abstract Syntax:] an appropriate representation in \hets for \freecad designs,
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder i.e., the \freecad abstract syntax (mostly done)
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder \item[Semantics:] \freecad terms should have a semantics in the sense of 3D Pointsets (see section \ref{sec:semantics})
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder \item[Import:] an import method translating \freecad documents into this
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc representation (partly done, has to be integrated into one method)
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc \item[\hets Integration:] a complete integration of the \freecad logic into the \hets
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc logic-graph (partly done, signature and simple static analysis missing)
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc \item[\hets tool:] a hook into the hets program to open \freecad documents from there, i.e., \bash{hets -g test.fcstd} should work
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc \item[Pretty printing] for basic \freecad specs, i.e.,
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc \haskell{Pretty}-instances for the \freecad abstract syntax
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\end{description}
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\subsection{Semantics}
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc\label{sec:semantics}
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen KuksaWe first give the semantics of some base objects such as rectangles,
d6ce032cac688f3698be7133d27f53d3967e6749Christian Maederboxes, and cylinders. The goal is to specify the semantics for each of
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucthe base objects used in the abstract syntax of \freecad and also for
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Lucthe transformation by rotations and translations as well as for
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luccompound objects such as \haskell{Cut}, \haskell{Common},
551f1476dea3f969775527cb15fd512e86279307Karl Luc\haskell{Fusion}, etc..
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\begin{align}
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\setsem{Rectangle(w, l)} & = \text{The set consisting of the four sides of the }\notag\\
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc & \qquad \text{rectangle in the x-y-plane}\notag\\
59ec6aa4da4c93d0d4ef53ed74fdf866d0654539Eugen Kuksa & = \setsep{(x,y,0)}{x\in[0,l], y\in\{0,w\}}\notag\\
59ec6aa4da4c93d0d4ef53ed74fdf866d0654539Eugen Kuksa & \quad \cup \setsep{(x,y,0)}{x\in\{0,l\}, y\in[0,w]}\\
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc\setsem{Box(h, l, w)} & = \text{The solid bounded by the faces of the box}\notag\\
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder & = [0,l]\times[0,w]\times[0,h]\\
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder\setsem{Cylinder(a, h, r)} & = \text{The ``pac-man'' cylinder along z-axis}\notag\\
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder & = circle\times[0,h]\\
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder \text{where}~ circle &=\setsep{(\rho\cdot cos(\alpha),\rho\cdot sin(\alpha))}{\alpha \in [0,a], \rho \in [0,r]}\notag\\
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Luc\setsem{Sphere(a_1, a_2, a_3, r)} & = \text{The intersection between a full sphere and a 'pac-man' cylinder}\notag\\
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc& \text {on the z-axis (which may cut a 'cake-slice' and also the nort-pole/south-pole caps)}\notag\\
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski& = \setsep{(x,y,z)}{x + y + z \leq r} \cap \notag\\
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa& \setsep{(\rho\cdot cos(\alpha),\rho\cdot sin(\alpha),z)}{z \in [sin(a_1),sin(a_2)]. \rho \in [0, \infty], \alpha \in [0, a_3]}\\
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc\setsem{Cone(a, r_1, r_2, h)} & = \text{The intersection between a fullright circular cone and a 'pac-man' cylinder}\notag\\
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc& = \setsep{(\rho \cdot cos(\alpha), \rho \cdot sin(\alpha), z)}{\rho \leq r_1 + {{z}\over{h}} \cdot (r_2 - r_1). z \in [0,h],\alpha \in [0, a]} \\
0b282d1269b8f9a658f7ce9090575ba1b00e8d66Christian Maeder\setsem{Torus(a_1, a_2, a_3, r_1, r_2)} & = \text{a bit trickier: union between a torus and a cylinder with the same center and the}\notag\\
d386b61802c70e3d220d4520d9fcdefbd9c469f4Soeren D. Schulze& \text {same symmetry axis all intersected with an infinite-radius z-axis centered 'pac-man' cylinder}\notag\\
0b282d1269b8f9a658f7ce9090575ba1b00e8d66Christian Maeder& = \{(x,y,z)\} \cup \{(x_2,y_2,z_2)\}\notag\\
0b282d1269b8f9a658f7ce9090575ba1b00e8d66Christian Maeder& \text{where:}\notag\\
52c81e62d4a3797b926fb3392369b45a9fef336cSoeren D. Schulze& circle = \setsep{(\rho\cdot cos(\alpha), \rho\cdot sin(\alpha))}{\alpha \in [a_1, a_2], \rho \in [0,r_2]}\notag\\
52c81e62d4a3797b926fb3392369b45a9fef336cSoeren D. Schulze& (rad, z) \in \setsep{(m,n)}{(-(m-r_1), n)\in circle}\notag\\
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder& x = rad\cdot cos (ang) \notag\\
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder& y = rad\cdot sin (ang) \notag\\
99a1bfbb82c875580410b4745617fea2297fdc2bEugen Kuksa& ang \in [0, a_3] \notag\\
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc& \text{if } (a_1 \geq -180) \text{or} (a_2 \leq 180) \text {then} \notag\\
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa& (x_2,y_2,z_2 - r_2 \cdot sin(a_1)) \in \notag\\
037be4e5b0e867dd148db2ea89640d8edf009053Eugen Kuksa&\setsem{Cone(a_3, r_1 - r_2 \cdot cos(a_1), r_1 - r_2 \cdot cos(a_2), sin(a_2) - sin(a_1))}\\
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa\setsem{Circle(sa, ea, r)} & = \setsep{(x,y,z)}{x = r\cdot cos(\alpha), y = r \cdot sin(\alpha), z = 0, \alpha \in [sa, ea]}\\
de03ed90ff6efbbc4751301bcf6b50d9790c1afbKarl Luc\end{document}