Д.ARMоед (30.07.2013 11:20 - 11:30, просмотров: 261) ответил Скрипач на Спасибо. А можно еще попросить вас добавить в этот пример управление устройством, имеющим свои собственные времянки? Например импульсное реле (включаем-выключаем импульсом 200мс, пауза не менее 400мс)?это ничего принципиально нового в обсуждение главного посыла (про два пальца) не добавит. Речь шла о том, что
1. возможно использование цикла Дейкстры для явного выделения предусловий и получения линейной записи. Ваш пример с прототридсами линейной записью никак не назовёшь. Зачем нужна линейная запись? Во-первых, все предусловия легко доступны для отдельной верификации, а это уже полрешения(второй половиной станут правильно выработанные постусловия). Во-вторых, чтобы иметь возможность легко написать что-то типа такого:
typedef void (code * FuncPtr)(int index); //указатель на функцию;
void Func_Caller(FuncPtr fn, int index)
{
(*fn)(index);
}
while (1) {//ахтунг! почти псевдокод:
if (Func_Caller(ThreadList.Current->PreCond_fn, ThreadList.Current->index))
Func_Caller(ThreadList.Current->fn, ThreadList.Current->index);
if (ThreadList.End) ThreadList.First() else ThreadList.Next();
}
2. использование WaitableObject's в любом виде - для события, сообщения, рандеву и т.п. требует введения серьёзной метамодели, которая не реализована в компиляторах императивных языков. Что-нибудь типа http://www.cwmforum.org/CwmAOM.pdf
p.s.: код (http://caxapa.ru/428651.html) д.б. поправлен, а то по-мелочи проморгал:
bool UartRead(){
PT_BEGIN();
while (true) {
// wait for sync byte
PT_WAIT_UNTIL(ReadByte(ch));
if (ch == Sync) {
// read length byte, ensure packet not too big
PT_WAIT_UNTIL(ReadByte(ch));
len = ch;
if (len <= MaxLength) {
// read n data bytes
for (i = 0; i < len; i++) {
PT_WAIT_UNTIL(ReadByte(ch));
data[i] = ch;
}
// read checksum, dispatch packet if valid
PT_WAIT_UNTIL(ReadByte(ch));
if (ValidChecksum(data, len, ch))
Dispatch(data, len);
} } }
PT_END();
}
while (1) {
if (GET_NEXT_BYTE) ReadByte(ch);
else if ((len <= MaxLength) && GET_PACKET) ReadPacket(len);
else if (ValidChecksum(data, len, ch) && GET_CHECKSUM) Dispatch(data, len);
else Log_Step();
}
static int receive_counter;
void ReadPacket(int num2read) {
switch READ_PACKET_STATE {
case 0:
receive_counter=0;
GET_NEXT_BYTE = 1;
READ_PACKET_STATE = 1;
break;
case 1:
data[receive_counter] = ch;
while (receive_counter < len) {
receive_counter++;
GET_NEXT_BYTE = 1;
return;
}
GET_NEXT_BYTE = 1; //добавлено: принять контрольную сумму
READ_PACKET_STATE = 2;
break;
case 2:
READ_PACKET_STATE = 0; //добавлено: сбросить автомат
GET_PACKET = 0;
GET_CHECKSUM = 1;
break;
default:
break;
}
}