216 lines
10 KiB
TeX
216 lines
10 KiB
TeX
\documentclass[a4paper,fontsize=14bp]{article}
|
||
|
||
\input{../common-preamble}
|
||
\input{../fancy-listings-preamble}
|
||
\input{../bmstu-preamble}
|
||
\numerationTop
|
||
|
||
\begin{document}
|
||
\thispagestyle{empty}
|
||
\makeBMSTUHeader
|
||
|
||
% ... работе, номер, тема, предмет, ?а, кто
|
||
\makeReportTitle{лабораторной}{4}{Исчисление дискретных событий}{Представление знаний в информационных системах}{}{И.И. Лычков}
|
||
\newpage
|
||
\thispagestyle{empty}
|
||
\tableofcontents
|
||
\newpage
|
||
\pagestyle{fancy}
|
||
\section{Цель}
|
||
Получение практических навыков моделирования дискретно-событийных систем на языке логического программирования.
|
||
|
||
\section{Задание}
|
||
В качестве исходных данных выдается словесное описание некоторой физической системы, а именно: общие правила её функционирования, состояние системы в начальный момент, список произошедших событий и вопрос относительно состояния одного из объектов системы в определенный момент времени. Также выдаются аксиомы исчисления дискретных событий. Требуется выделить в исходном описании все объекты, события, флюенты, придумать для них идентификаторы в программе, затем представить логику функционирования заданной системы в виде программы на языке ASP программирования наборов решений с помощью аксиом исчисления дискретных событий, отладить работу программы так, чтобы она выдавала ответ на указанный в задании вопрос относительно состояния одного из объектов системы в определенный момент времени.
|
||
|
||
\section{Выполнение}
|
||
\subsection{Словесное описание системы согласно варианту}
|
||
Имеется две аксиомы initiates и terminates. Если агент включает нагреватель воздушного шара, то нагреватель более не будет выключен и будет включен. Мы задаем глобальное ограничение о том, что воздушный шар не может находиться одновременно на двух разных высотах в один момент времени.
|
||
|
||
Когда нагреватель включен, высота воздушного шара изменяется по закону:
|
||
\[h(t) = h(0) + V*t\]
|
||
Когда нагреватель выключен, высота воздушного шара изменяется по закону:
|
||
\[h(t) = h(0) - V*t,\]
|
||
где V = 1 - скорость воздушного шара (задана константой)
|
||
|
||
Высота воздушного шара освобождается от закона инерции по событиям включения и выключения нагревателя. Имеем следующие факты и хронику событий. Воздушный шар изначально находится на нулевой высоте. В момент времени 1 нагреватель включают, а в момент времени 3 нагреватель выключают. Необходимо проверить, что в момент времени 3 высота воздушного шара равна 2V, а в момент времени 4 она равна V.
|
||
\subsection{Перечень всех объектов, событий и флюентов с указанием их идентификаторов и смысловой нагрузки}
|
||
События и флюенты в программе:
|
||
\begin{itemize}
|
||
\item \verb|turnOn| - событие включения нагревателя;
|
||
\item \verb|turnOff| - событие выключения нагревателя;
|
||
\item \verb|heating| - флюент, говорящий о том, что шар нагревается и летит вверх;
|
||
\item \verb|falling| - флюент, говорящий о том, что шар охлаждается и падает;
|
||
\item \verb|height(X)| - флюент, говорящий о текущей высоте шара.
|
||
\end{itemize}
|
||
|
||
Имеется две аксиомы initiates и terminates.
|
||
\begin{verbatim}
|
||
initiates(turnOn, heating, Time) :- times(Time).
|
||
terminates(turnOff, heating, Time) :- times(Time).
|
||
|
||
initiates(turnOff, falling, Time) :- times(Time).
|
||
terminates(turnOn, falling, Time) :- times(Time).
|
||
\end{verbatim}
|
||
|
||
Мы задаем глобальное ограничение о том, что воздушный шар не может находиться одновременно на двух разных высотах в один момент времени.
|
||
\begin{verbatim}
|
||
:- holdsAt(height(X1), T), holdsAt(height(X2), T), X1 != X2.
|
||
\end{verbatim}
|
||
|
||
Имеем две аксиомы типа trajectory, описывающие поведение шара при нагревании и охлаждении:
|
||
\begin{verbatim}
|
||
trajectory(heating, T1, height(X2), T2) :-
|
||
times(T1), times(T2), T1 < T2,
|
||
holdsAt(height(X),T1),
|
||
X2 = X + 1 * (T2 - T1).
|
||
|
||
trajectory(falling, T1, height(X2), T2) :-
|
||
times(T1), times(T2), T1 < T2,
|
||
holdsAt(height(X),T1),
|
||
X2 = X - 1 * (T2 - T1).
|
||
\end{verbatim}
|
||
|
||
Высота воздушного шара освобождается от закона инерции по событиям включения и выключения нагревателя:
|
||
\begin{verbatim}
|
||
releases(turnOff, height(X), T) :- holdsAt(height(X), T).
|
||
releases(turnOn, height(X), T) :- holdsAt(height(X), T).
|
||
\end{verbatim}
|
||
|
||
Имеем следующие факты и хронику событий. Воздушный шар изначально находится на нулевой высоте, в момент времени 1 нагреватель включают, а в момент времени 3 нагреватель выключают:
|
||
\begin{verbatim}
|
||
initiallyP(height(0)).
|
||
initiallyN(heating).
|
||
|
||
happens(turnOn, 1).
|
||
happens(turnOff, 3).
|
||
\end{verbatim}
|
||
|
||
Необходимо проверить, что в момент времени 3 высота воздушного шара равна 2V, а в момент времени 4 она равна V.
|
||
\begin{verbatim}
|
||
info(F1, T1, F2, T2) :-
|
||
holdsAt(height(F1), T1), holdsAt(height(F2), T2),
|
||
F1==2, T1==3, F2 == 1, T2 == 4.
|
||
#show info/4.
|
||
\end{verbatim}
|
||
\subsection{Результат выполнение программы}
|
||
Результат выполнения программы представлен на рисунке \hrf{pic:result}.
|
||
\begin{figure}[H]
|
||
\centering
|
||
\includegraphics[height=6cm]{04-lab-result.png}
|
||
\caption{Результаты работы программы}
|
||
\label{pic:result}
|
||
\end{figure}
|
||
|
||
На рисунке \hrf{pic:result} видно, что программа нашла одно сочетание флюентов и временных отметок: в момент времени 3 высота воздушного шара равна 2, а в момент времени 4 она равна 1.
|
||
|
||
\newpage
|
||
\appendix
|
||
\setcounter{secnumdepth}{0}
|
||
\section*{Приложения}
|
||
\addcontentsline{toc}{section}{Приложения}
|
||
\renewcommand{\thesubsection}{\Alph{subsection}}
|
||
|
||
\setcounter{secnumdepth}{5}
|
||
\subsection{Полный листинг приложения по индивидуальному заданию}
|
||
\begin{lstlisting}[language=C,style=CCodeStyle]
|
||
%*
|
||
********************************************************************
|
||
Стандартные аксиомы исчисления дискретных событий.
|
||
********************************************************************
|
||
*%
|
||
|
||
%% BEC1 - StoppedIn(t1,f,t2)
|
||
stoppedIn(T1,Fluent,T2) :-
|
||
times(T1), times(T2), T1<T2,
|
||
terminates(Event,Fluent,T),
|
||
happens(Event,T), T1<T, T<T2.
|
||
|
||
stoppedIn(T1,Fluent,T2) :-
|
||
times(T1), times(T2), T1<T2,
|
||
releases(Event,Fluent,T),
|
||
happens(Event,T), T1<T, T<T2.
|
||
|
||
%% BEC2 - StartedIn(t1,f,t2)
|
||
startedIn(T1,Fluent,T2) :-
|
||
times(T1), times(T2), T1<T2,
|
||
initiates(Event,Fluent,T),
|
||
happens(Event,T), T1<T, T<T2.
|
||
|
||
startedIn(T1,Fluent,T2) :-
|
||
times(T1), times(T2), T1<T2,
|
||
releases(Event,Fluent,T),
|
||
happens(Event,T), T1<T, T<T2.
|
||
|
||
%% BEC3 - HoldsAt(f,t)
|
||
holdsAt(Fluent2,T2) :-
|
||
times(T1),
|
||
happens(Event,T1),
|
||
initiates(Event,Fluent1,T1),
|
||
trajectory(Fluent1,T1,Fluent2,T2),
|
||
not stoppedIn(T1,Fluent1,T2).
|
||
|
||
%% BEC4 - HoldsAt(f,t)
|
||
holdsAt(Fluent,T) :-
|
||
times(T),
|
||
initiallyP(Fluent),
|
||
not stoppedIn(0,Fluent,T).
|
||
|
||
%% BEC5 - not HoldsAt(f,t)
|
||
-holdsAt(Fluent,T):-
|
||
times(T),
|
||
initiallyN(Fluent),
|
||
not startedIn(0,Fluent,T).
|
||
|
||
%% BEC6 - HoldsAt(f,t)
|
||
holdsAt(Fluent,T) :-
|
||
times(T),
|
||
happens(Event,T1),
|
||
initiates(Event,Fluent,T1), T1<T,
|
||
not stoppedIn(T1,Fluent,T).
|
||
|
||
%% BEC7 - not HoldsAt(f,t)
|
||
-holdsAt(Fluent,T):-
|
||
times(T),
|
||
happens(Event,T1),
|
||
terminates(Event,Fluent,T1), T1<T,
|
||
not startedIn(T1,Fluent,T).
|
||
|
||
times(0..5).
|
||
|
||
initiates(turnOn, heating, Time) :- times(Time).
|
||
terminates(turnOff, heating, Time) :- times(Time).
|
||
|
||
initiates(turnOff, falling, Time) :- times(Time).
|
||
terminates(turnOn, falling, Time) :- times(Time).
|
||
|
||
releases(turnOff, height(X), Time) :- holdsAt(height(X), Time).
|
||
releases(turnOn, height(X), Time) :- holdsAt(height(X), Time).
|
||
|
||
trajectory(heating, T1, height(X2), T2) :-
|
||
times(T1), times(T2), T1 < T2,
|
||
holdsAt(height(X),T1),
|
||
X2 = X + 1 * (T2 - T1).
|
||
|
||
trajectory(falling, T1, height(X2), T2) :-
|
||
times(T1), times(T2), T1 < T2,
|
||
holdsAt(height(X),T1),
|
||
X2 = X - 1 * (T2 - T1).
|
||
|
||
:- holdsAt(height(X1), T), holdsAt(height(X2), T), X1 != X2.
|
||
|
||
releases(turnOn, heating, Time) :- times(Time).
|
||
releases(turnOff, heating, Time) :- times(Time).
|
||
|
||
initiallyP(height(0)).
|
||
initiallyN(heating).
|
||
|
||
happens(turnOn, 1).
|
||
happens(turnOff, 3).
|
||
|
||
info(F1, T1, F2, T2) :- holdsAt(height(F1), T1), holdsAt(height(F2), T2), F1==2, T1==3, F2 == 1, T2 == 4.
|
||
#show info/4.
|
||
\end{lstlisting}
|
||
|
||
\end{document}
|
||
|